Documentation

CsdLean4.Empirical.CSD.Gates.MultiQubit

Empirical/CSD: Multi-qubit gates (CSD-side reading) #

Category: 3-Local (CSD-side companion to Empirical/QM/Gates/MultiQubit.lean).

Two CSD realisability claims (Toffoli, Fredkin) on the 3-qubit space, plus identity-transport re-exports. Same template as Empirical/CSD/Gates/{SingleQubit,TwoQubit}.lean, specialised to N = 3 (Hilbert space EuclideanSpace ℂ (Fin 8)).

LF4 obligations #

LF4-todo §13.2 per gate. DISCHARGED 2026-07-19 on cpSectorData (Gates/MultiQubitDischarge.lean: toffoli_/fredkin_realisable_cpSector), modulo the posited CSD sector (SO-1); U_isometry derived from the gate ∈ U(8). Honest scope (PLACEHOLDERS.md §7): the bundle type carries no Σ-flow, so this discharges the Prop as-typed, not the Σ-flow-lift prose (open D1 gap). See BRIDGE-OBLIGATIONS.md §2.6, PLACEHOLDERS.md §1.

source
def CSD.Empirical.CSDBridge.Gates.MultiQubit.toffoli_realisable_for {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : LF2.SectorData SigmaSpace P G) :
Prop

PLACEHOLDER (Prop definition, not proved). CSD realisability for Toffoli (CCNOT). See PLACEHOLDERS.md.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def CSD.Empirical.CSDBridge.Gates.MultiQubit.fredkin_realisable_for {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : LF2.SectorData SigmaSpace P G) :
    Prop

    PLACEHOLDER (Prop definition, not proved). CSD realisability for Fredkin (CSWAP). See PLACEHOLDERS.md.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Identity-transport re-exports #

      source
      theorem CSD.Empirical.CSDBridge.Gates.MultiQubit.csd_qmToffoli_mul_self :
      QM.Gates.qmToffoli * QM.Gates.qmToffoli = 1

      Toffoli is involutive (re-export).

      source
      theorem CSD.Empirical.CSDBridge.Gates.MultiQubit.csd_qmFredkin_mul_self :
      QM.Gates.qmFredkin * QM.Gates.qmFredkin = 1

      Fredkin is involutive (re-export).