LedgerComplete
plain-language theorem explainer
LedgerComplete encodes the closure axiom for a geometric scale sequence: the sum of scales at any two indices must equal the scale at some third index. Researchers deriving the golden ratio from additive ledger composition in Recognition Science cite this definition when moving from the three axioms to r² = r + 1. The body is a direct forall-exists statement over the scale function with no lemmas or tactics applied.
Claim. Let $S$ be a geometric scale sequence with ratio $r > 0$, $r ≠ 1$. Then $S$ satisfies ledger completeness when for all natural numbers $n, m$ there exists a natural number $k$ such that $r^n + r^m = r^k$.
background
The module derives $r^2 = r + 1$ from three axioms: a discrete geometric scale sequence, additive composition of ledger entries (motivated by the additivity of the J-cost function $J(x) = ½(x + 1/x) - 1$), and closure under composition. GeometricScaleSequence is the structure that records a ratio $r > 0$ with $r ≠ 1$ together with the noncomputable scale function returning $r$ raised to the index. The local theoretical setting is the T5-to-T6 bridge in which J-uniqueness forces the self-similar fixed point; the module documentation states that the deeper origin of closure itself is treated in HierarchyDynamics via the Fibonacci recurrence from uniform scaling and local binary posting.
proof idea
This is a definition whose body is the literal forall-exists statement on the scale function. No lemmas are invoked and no tactics are used; the accompanying comment simply records that the full closure is stronger than required and that the minimal case (n=0, m=1 implying k=2) already forces the golden ratio.
why it matters
The definition supplies the exact meaning of closure needed to extract $r^2 = r + 1$ and thereby identify the ratio with the golden ratio phi in the T5-to-T6 step. It sits inside the chain that begins with the three axioms listed in the module documentation and feeds the subsequent derivations of phi_forcing_complete and closed_ratio_is_phi among the sibling declarations. The module documentation notes that the physical necessity of closure is left to HierarchyDynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.