Documentation

CsdLean4.Empirical.CSD.Gates.BellPrep

Empirical/CSD: Bell-state preparation circuit (CSD-side reading) #

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

Tests the CSDUnitaryBundle.comp composition pattern: a Hadamard bundle on qubit 0 composes with a CNOT bundle on qubits (0, 1) to yield a CSD bundle for the full Bell-state preparation circuit.

What this file shows #

Given two CSD unitary bundles b_H : CSDUnitaryBundle D 2 H_4 (the Hadamard ⊗ Identity bundle on the 2-qubit space) and b_CNOT : CSDUnitaryBundle D 2 H_4 (the CNOT bundle), their composition b_CNOT.comp b_H is a CSD bundle for the Bell-state preparation circuit CNOT ∘ (H ⊗ I).

LF4 obligations #

Same per-gate LF4-todo §13.2 obligations as the individual gates. The composition does not add a new obligation — it inherits the two underlying gates' obligations via CSDUnitaryBundle.comp.

Honest reading #

This file tests the composition lemma CSDUnitaryBundle.comp from Empirical/CSD/Gates/Framework.lean. The Hilbert-side identity (CNOT ∘ (H ⊗ I)) |00⟩ = |Φ⁺⟩ is established (or, in this commit, declared but deferred) on the QM side and not re-derived here. The CSD-side content is the bundle-composition structure plus the existence-conditional-on-LF4 commitment that the resulting bundle's U is ontic-realisable.

source
def CSD.Empirical.CSDBridge.Gates.BellPrep.bell_prep_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).

Bell-state preparation circuit realisability: there exist CSD unitary bundles for the Hadamard-on-qubit-0 operation H ⊗ I and for CNOT, whose U fields agree with the QM-side gate matrices. The bundle composition b_CNOT.comp b_HI then realises the Bell-state preparation circuit.

Status: DISCHARGED 2026-07-19 on the concrete cpSectorData (Gates/BellPrepDischarge.lean: bell_prep_realisable_cpSector), modulo the posited CSD sector (SO-1). Both bundle existences (H ⊗ I and CNOT) are supplied with U the gate action and U_isometry derived from U(4) membership. This is the ninth and last of the gate realisability Props to be discharged. Honest scope (PLACEHOLDERS.md §7): the bundle type carries U + U_isometry + a Context, not a Σ-flow, so this discharges the Prop as typed, not the Σ-flow-lift prose (the open D1 gap). See PLACEHOLDERS.md §1 for the canonical ledger.

The earlier formulation ∃ b_HI b_CNOT, True was a vacuous Prop (satisfied by any two bundles); rewritten 2026-05-22 to constrain both bundles' U to the QM-side matrices, making the Prop non-vacuous.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def CSD.Empirical.CSDBridge.Gates.BellPrep.bell_prep_compose {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} (b_HI b_CNOT : CSDUnitaryBundle D 2 (EuclideanSpace ℂ (Fin 4))) :
    CSDUnitaryBundle D 2 (EuclideanSpace ℂ (Fin 4))

    Composition instance. Given two CSDUnitaryBundles on the same context + qubit count, their comp is well-defined. Just re-exports CSDUnitaryBundle.comp for the Bell-prep use case; guarantees the composition is mechanical.

    Equations
    Instances For

      QM-side re-exports #

      source
      theorem CSD.Empirical.CSDBridge.Gates.BellPrep.csd_qmBellPrep_factorisation :
      QM.Gates.qmBellPrepCircuit = QM.Gates.qmCNOT * QM.Gates.qmH_tensor_I

      TRANSPORT-ONLY: re-export of the QM-side factorisation handle. Definitional unfold; see PLACEHOLDERS.md §3.

      source
      theorem CSD.Empirical.CSDBridge.Gates.BellPrep.csd_qmBellPrep_yields_phiplus :
      (Matrix.toEuclideanLin QM.Gates.qmBellPrepCircuit) QM.Gates.qmKet00 = QM.Gates.qmKetPhiPlus

      TRANSPORT-ONLY: re-export of the QM-side Bell-prep headline identity. (CNOT ∘ (H ⊗ I)) |00⟩ = |Φ⁺⟩; proof body in Empirical/QM/Gates/BellPrep.lean.