Empirical/CSD/Gates: §13.2 discharge for Bell-state preparation (H⊗I, CNOT)

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

Completes the gate *_realisable_for discharge (PLACEHOLDERS.md §1, the ninth and last Prop). bell_prep_realisable_for asks for two CSDUnitaryBundles realising H ⊗ I and CNOT; both are discharged on cpSectorData p₀ (p₀ : CPN 4). qmCNOT ∈ U(4) is reused from TwoQubitDischarge; qmH_tensor_I (= H ⊗ I, real Hermitian, involutive) is shown unitary here (qmH_tensor_I_mem_unitaryGroup). Each U_isometry is derived from U(4) membership via inner_toEuclideanLin_unitary.

Honest scope

As in 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). With this file all nine gate realisability Props are discharged on the concrete instance.

References: Gates/{SingleQubit,TwoQubit,MultiQubit}Discharge.lean, Empirical/QM/Gates/BellPrep.lean (qmH_tensor_I), PLACEHOLDERS.md §1/§7.

theorem CSD.LF4.qmH_tensor_I_hermitian : star Empirical.QM.Gates.qmH_tensor_I = Empirical.QM.Gates.qmH_tensor_I

H ⊗ I is Hermitian (real symmetric): star (H⊗I) = H⊗I.

theorem CSD.LF4.qmH_tensor_I_mul_self : Empirical.QM.Gates.qmH_tensor_I * Empirical.QM.Gates.qmH_tensor_I = 1

H ⊗ I is involutive: (H⊗I)² = 1.

theorem CSD.LF4.qmH_tensor_I_mem_unitaryGroup : Empirical.QM.Gates.qmH_tensor_I ∈ Matrix.unitaryGroup (Fin 4) ℂ

qmH_tensor_I ∈ U(4) (Hermitian involution: (H⊗I) · star(H⊗I) = (H⊗I)² = 1).

theorem CSD.LF4.bell_prep_realisable_cpSector (p₀ : CPN 4) : Empirical.CSDBridge.Gates.BellPrep.bell_prep_realisable_for (cpSectorData p₀)

§13.2 discharge (Bell-state preparation). bell_prep_realisable_for (cpSectorData p₀) holds: bundles realising H ⊗ I and CNOT, each U_isometry derived from U(4) membership. Modulo the posited CSD sector (SO-1). The ninth and last gate realisability Prop.