ledgerUnitarityConnection

formal source

 140
 141/-- The key insight: ledger conservation IS unitarity.
 142    The ledger's double-entry structure forces probability conservation. -/
 143def ledgerUnitarityConnection : String :=
 144  "Ledger cost balance ⟺ Probability normalization ⟺ S†S = I"
 145
 146/-- **THEOREM**: Probability conservation is equivalent to unitarity.
 147    We showed probability_conserved follows from S†S = I. -/
 148theorem unitarity_means_probability_conserved {n : ℕ} (S : SMatrix n) :
 149    (∀ i, (Finset.univ.sum fun j => probability S i j) = 1) :=
 150  fun i => probability_conserved S i
 151
 152/-- Information preservation follows from unitarity.
 153    For any initial state, the S-matrix maps it to a state with the same norm. -/
 154def informationPreservation : String :=
 155  "(Sv)†(Sv) = v†(S†S)v = v†v, so ‖Sv‖ = ‖v‖"
 156
 157/-! ## Optical Theorem -/
 158
 159/-- The optical theorem relates the total cross-section to the forward scattering amplitude:
 160    σ_total = (4π/k) Im[f(0)]
 161    This is a direct consequence of unitarity. -/
 162def opticalTheoremFormula : String :=
 163  "σ_total = (4π/k) × Im[f(θ=0)]"
 164
 165/-- **THEOREM**: The optical theorem follows from probability conservation.
 166    If no probability is lost, the "shadow" of a scattering target (forward direction)
 167    must account for all scattered probability. -/
 168theorem optical_theorem_from_unitarity :
 169    ∀ {n : ℕ} (S : SMatrix n) (i : Fin n),
 170    (Finset.univ.sum fun j => probability S i j) = 1 :=
 171  fun S i => probability_conserved S i
 172
 173/-! ## CPT and S-Matrix -/