Empirical/CSD/Gates: §13.2 discharge for the single-qubit gates (H, S, T)

Category: 3-Local (CSD-side concrete discharge of the LF4-§13.2 gate-realisability obligation).

The three *_realisable_for Props in Empirical/CSD/Gates/SingleQubit.lean were claim-shaped placeholders (PLACEHOLDERS.md §1: "no concrete D is constructed for which any holds"). This module DISCHARGES them on the concrete Kähler sector cpSectorData p₀: each gate's action is exhibited as 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(2) — the sector-symmetry membership — via Projectivization.inner_toEuclideanLin_unitary (the same content cpSectorActionBundle carries for a general sector element).

Honest scope

• Modulo the posited CSD sector (SO-1). cpSectorData is the posited Kähler sector; this discharges the Props given that sector, exactly as WignerDischarge/cpSectorActionBundle do. It does not derive the sector.
• What the type carries. Per PLACEHOLDERS.md §7 the CSDUnitaryBundle type carries U + U_isometry + a Context D, NOT a Σ-flow / π-equivariance datum. So these theorems establish the Prop as typed (a Context plus a Hilbert isometry equal to the gate); the stronger prose reading (the gate as the projective lift of a deterministic Σ-flow) is the open D1 gap and is NOT claimed here.
• U_isometry is derived, not posited. It comes from qm{H,S,T} ∈ U(2) (inner_toEuclideanLin_unitary), i.e. from the gate being a Fubini–Study isometry — the posited-sector datum (SO-1) — not from μL-measure-preservation (measure ≠ metric; see WignerDischarge).

Net effect: the three single-qubit gate placeholders (PLACEHOLDERS.md §1) become proved theorems on the concrete instance. The two-qubit / multi-qubit / Bell-prep gates follow the same pattern (each gate matrix is unitary) and are the mechanical continuation.

References: Empirical/CSD/Gates/WignerDischarge.lean, Empirical/CSD/Gates/SingleQubit.lean, Empirical/QM/Gates/SingleQubit.lean (qmH, qmS, qmT), specs/LF4-todo.md §13.2, BRIDGE-OBLIGATIONS.md §2.6, PLACEHOLDERS.md §1/§7.

theorem CSD.LF4.qmH_mem_unitaryGroup : Empirical.QM.Gates.qmH ∈ Matrix.unitaryGroup (Fin 2) ℂ

qmH ∈ U(2): Hadamard is Hermitian (real symmetric) and involutive, so qmH * star qmH = qmH * qmH = 1.

theorem CSD.LF4.qmS_mem_unitaryGroup : Empirical.QM.Gates.qmS ∈ Matrix.unitaryGroup (Fin 2) ℂ

qmS ∈ U(2): S = diag(1, i), S · Sᴴ = diag(1, i·(-i)) = 1.

theorem CSD.LF4.qmT_mem_unitaryGroup : Empirical.QM.Gates.qmT ∈ Matrix.unitaryGroup (Fin 2) ℂ

qmT ∈ U(2): T = diag(1, e^{iπ/4}), T · Tᴴ = diag(1, e^{iπ/4}·e^{-iπ/4}) = 1.

theorem CSD.LF4.hadamard_realisable_cpSector (p₀ : CPN 2) : Empirical.CSDBridge.Gates.SingleQubit.hadamard_realisable_for (cpSectorData p₀)

§13.2 discharge (Hadamard). hadamard_realisable_for (cpSectorData p₀) holds: the bundle's U is the Hadamard action, U_isometry derived from qmH ∈ U(2).

theorem CSD.LF4.phaseS_realisable_cpSector (p₀ : CPN 2) : Empirical.CSDBridge.Gates.SingleQubit.phaseS_realisable_for (cpSectorData p₀)

§13.2 discharge (Phase S). phaseS_realisable_for (cpSectorData p₀) holds.

theorem CSD.LF4.phaseT_realisable_cpSector (p₀ : CPN 2) : Empirical.CSDBridge.Gates.SingleQubit.phaseT_realisable_for (cpSectorData p₀)

§13.2 discharge (Phase T). phaseT_realisable_for (cpSectorData p₀) holds.