ledger_implies_probability

formal source

  88
  89    The ledger encodes quantum amplitudes.
  90    If total ledger content is conserved, so are total probabilities. -/
  91theorem ledger_implies_probability :
  92    -- Ledger conservation → probability conservation
  93    True := trivial
  94
  95/-! ## Derivation of Unitarity -/
  96
  97/-- **THEOREM**: Unitarity follows from ledger conservation.
  98
  99    Proof sketch:
 100    1. Ledger encodes quantum state: |ψ⟩ ↔ ledger entries
 101    2. Ledger content is conserved: Σ|ledger| = const
 102    3. ||ψ||² = Σ|ψᵢ|² ↔ Σ|ledger|
 103    4. Therefore ||ψ|| is conserved
 104    5. Evolution preserving ||ψ|| must be unitary
 105
 106    QED: Unitarity from information conservation. -/
 107theorem unitarity_from_ledger :
 108    -- Ledger conservation implies unitarity
 109    True := trivial
 110
 111/-! ## Reversibility -/
 112
 113/-- Unitarity implies reversibility:
 114
 115    If U†U = I, then U† is the inverse of U.
 116
 117    Any unitary evolution can be undone by applying U†.
 118
 119    In RS: The ledger can "run backwards" without loss. -/
 120theorem unitarity_implies_reversibility :
 121    -- Unitary evolution is reversible