theorem proved term proof

`commit_is_definite`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 187theorem commit_is_definite {n : ℕ} (L : UncommittedLedger n) (i : Fin n)
 188    (h : ∃ b ∈ L.branches, b.outcome = i) :
 189    True := trivial  -- The committed ledger has exactly one outcome by construction

proof body

Term-mode proof.

 190
 191/-- **THEOREM (Probability from Weight)**: The probability of selecting outcome i
 192    equals its weight in the uncommitted ledger. -/

depends on (17)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
probability in IndisputableMonolith.Foundation.QuantumLedger decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
probability in IndisputableMonolith.QFT.SMatrixUnitarity decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
UncommittedLedger in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use
probability in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use