Empirical/CSD/Gates: §13.2 discharge for the multi-qubit gates (Toffoli, Fredkin)

Category: 3-Local (CSD-side concrete discharge of LF4-§13.2, multi-qubit tier).

Companion to Gates/{SingleQubit,TwoQubit}Discharge.lean. The two three-qubit gate *_realisable_for Props (Empirical/CSD/Gates/MultiQubit.lean) were claim-shaped placeholders (PLACEHOLDERS.md §1). This module DISCHARGES them on cpSectorData p₀ (p₀ : CPN 8): each gate's action is a genuine CSDUnitaryBundle whose U IS the gate and whose U_isometry is derived from the gate lying in U(8) (inner_toEuclideanLin_unitary). Toffoli and Fredkin are real Hermitian permutation involutions, so Gᴴ * G = 1 (qmG_unitary) gives membership directly.

Honest scope

Identical to the earlier tiers: modulo the posited CSD sector (SO-1); the bundle type carries U + U_isometry

• a Context, not a Σ-flow (PLACEHOLDERS.md §7), so this discharges the Prop as typed, not the Σ-flow-lift prose (open D1 gap). U_isometry is derived from qm{Toffoli,Fredkin} ∈ U(8) (sector-symmetry membership), not μL-measure-preservation.

References: Gates/SingleQubitDischarge.lean, Empirical/QM/Gates/MultiQubit.lean (qmToffoli, qmFredkin, qmG_unitary), PLACEHOLDERS.md §1/§7.

theorem CSD.LF4.qmToffoli_mem_unitaryGroup : Empirical.QM.Gates.qmToffoli ∈ Matrix.unitaryGroup (Fin 8) ℂ

qmToffoli ∈ U(8): Toffoliᴴ * Toffoli = 1 (Hermitian involution).

theorem CSD.LF4.qmFredkin_mem_unitaryGroup : Empirical.QM.Gates.qmFredkin ∈ Matrix.unitaryGroup (Fin 8) ℂ

qmFredkin ∈ U(8): Fredkinᴴ * Fredkin = 1.

theorem CSD.LF4.toffoli_realisable_cpSector (p₀ : CPN 8) : Empirical.CSDBridge.Gates.MultiQubit.toffoli_realisable_for (cpSectorData p₀)

§13.2 discharge (Toffoli). toffoli_realisable_for (cpSectorData p₀) holds.

theorem CSD.LF4.fredkin_realisable_cpSector (p₀ : CPN 8) : Empirical.CSDBridge.Gates.MultiQubit.fredkin_realisable_for (cpSectorData p₀)

§13.2 discharge (Fredkin). fredkin_realisable_for (cpSectorData p₀) holds.