Documentation

CsdLean4.Empirical.CSD.Gates.TwoQubit

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

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

Three CSD realisability claims, one per gate, plus identity-transport re-exports. Same template as Empirical/CSD/Gates/SingleQubit.lean, specialised to N = 2 (Hilbert space EuclideanSpace ℂ (Fin 4)).

LF4 obligations #

LF4-todo §13.2 (per gate; same as single-qubit gates, instantiated at N = 2). DISCHARGED 2026-07-19 on cpSectorData (Gates/TwoQubitDischarge.lean: cnot_/swap_/cz_realisable_cpSector), modulo the posited CSD sector (SO-1); U_isometry derived from the gate ∈ U(4). 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.TwoQubit.cnot_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 CNOT. See PLACEHOLDERS.md.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def CSD.Empirical.CSDBridge.Gates.TwoQubit.swap_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 SWAP. See PLACEHOLDERS.md.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CSD.Empirical.CSDBridge.Gates.TwoQubit.cz_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 CZ. 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.TwoQubit.csd_qmCNOT_mul_self :
        QM.Gates.qmCNOT * QM.Gates.qmCNOT = 1

        CNOT is involutive (re-export).

        source
        theorem CSD.Empirical.CSDBridge.Gates.TwoQubit.csd_qmSWAP_mul_self :
        QM.Gates.qmSWAP * QM.Gates.qmSWAP = 1

        SWAP is involutive (re-export).

        source
        theorem CSD.Empirical.CSDBridge.Gates.TwoQubit.csd_qmCZ_mul_self :
        QM.Gates.qmCZ * QM.Gates.qmCZ = 1

        CZ is involutive (re-export).