No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
91theorem ledger_implies_probability :
92 -- Ledger conservation → probability conservation
93 True := trivial
proof body
Term-mode proof.
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. -/
depends on (14)
Lean names referenced from this declaration's body.
-
const
in IndisputableMonolith.Action.PathSpace
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
probability
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
probability
in IndisputableMonolith.QFT.SMatrixUnitarity
decl_use
-
probability
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use