Empirical/CSD/Gates: §13.2 discharge for the two-qubit gates (CNOT, SWAP, CZ) #
Category: 3-Local (CSD-side concrete discharge of the LF4-§13.2 gate-realisability obligation, two-qubit tier).
Companion to Gates/SingleQubitDischarge.lean. The three two-qubit gate
*_realisable_for Props (Empirical/CSD/Gates/TwoQubit.lean) were claim-shaped
placeholders (PLACEHOLDERS.md §1). This module DISCHARGES them on the concrete Kähler
sector cpSectorData p₀ (p₀ : CPN 4): each gate's action is a genuine CSDUnitaryBundle
whose U IS the gate's Hilbert action and whose U_isometry is a THEOREM, derived from the
gate lying in U(4) (inner_toEuclideanLin_unitary). CNOT, SWAP, CZ are real Hermitian
permutation/diagonal involutions, so Gᴴ * G = 1 (qmG*_unitary) gives membership directly.
Honest scope #
Identical to the single-qubit tier: modulo the posited CSD sector (SO-1) (the sector is posited), and per
PLACEHOLDERS.md §7 the CSDUnitaryBundle type carries U + U_isometry + a Context,
not a Σ-flow — so these theorems establish the Prop as typed, not the stronger Σ-flow-lift
prose (the open D1 gap). U_isometry is derived from qm{CNOT,SWAP,CZ} ∈ U(4) — the
sector-symmetry (Fubini–Study isometry) membership — not from μL-measure-preservation.
References: Gates/SingleQubitDischarge.lean, Empirical/CSD/Gates/TwoQubit.lean,
Empirical/QM/Gates/TwoQubit.lean (qmCNOT, qmSWAP, qmCZ, qmG*_unitary),
specs/LF4-todo.md §13.2, PLACEHOLDERS.md §1/§7.
qmCNOT ∈ U(4): CNOTᴴ * CNOT = 1 (Hermitian involution).
qmSWAP ∈ U(4): SWAPᴴ * SWAP = 1.
qmCZ ∈ U(4): CZᴴ * CZ = 1.
§13.2 discharge (CNOT). cnot_realisable_for (cpSectorData p₀) holds: the bundle's
U is the CNOT action, U_isometry derived from qmCNOT ∈ U(4). Modulo the posited CSD sector (SO-1).
§13.2 discharge (SWAP). swap_realisable_for (cpSectorData p₀) holds.
§13.2 discharge (CZ). cz_realisable_for (cpSectorData p₀) holds.