def definition def or abbrev

`LedgerComplete`

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

formal statement (Lean)

 239def LedgerComplete (S : GeometricScaleSequence) : Prop :=

proof body

Definition body.

 240  ∀ n m : ℕ, ∃ k : ℕ, S.scale n + S.scale m = S.scale k
 241
 242/-- Full closure is too strong for arbitrary n, m.
 243    But the MINIMAL closure (n=0, m=1 → k=2) is achievable
 244    and forces the golden ratio. -/

depends on (10)

Lean names referenced from this declaration's body.

scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
forces in IndisputableMonolith.Foundation.MagnitudeOfMismatch decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
GeometricScaleSequence in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use