minimal_closure_sufficient
plain-language theorem explainer
The minimal closure condition on a geometric scale sequence is equivalent to the algebraic relation 1 + r = r². Researchers deriving the golden ratio from ledger axioms in Recognition Science would cite this equivalence as the bridge from closure to the self-similar fixed point. The proof is a direct term-mode reduction that unfolds the isClosed predicate and ledger composition definition then applies reflexivity.
Claim. Let $S$ be a geometric scale sequence with positive ratio $r > 0$, $r ≠ 1$. Then $S$ is minimally closed if and only if $1 + r = r^2$.
background
A GeometricScaleSequence is a structure holding a ratio $r > 0$ with $r ≠ 1$, together with the scale function that returns $r^n$ for each natural number $n$. The module derives $r^2 = r + 1$ from three axioms: discrete geometric scaling of recognition events, additive ledger composition (required because J-cost is additive), and closure under composition (the composed scale must lie in the sequence). The local setting is the T5-to-T6 segment of the forcing chain, where J-uniqueness (J(x) = (x + x^{-1})/2 - 1) already supplies additivity and the present result supplies the minimal algebraic constraint that forces the fixed point phi.
proof idea
The proof is a one-line term-mode wrapper. It introduces the sequence S, unfolds the definitions of isClosed and ledgerCompose, and concludes by reflexivity.
why it matters
This result shows that the minimal (n=0, m=1 to k=2) closure condition already forces the golden-ratio equation, completing the local step from ledger completeness to phi as the self-similar fixed point in the T5–T6 bridge. It sits inside the larger derivation chain that obtains D = 3 and the eight-tick octave from the Recognition Composition Law. The module doc notes that the deeper justification for why closure must hold is deferred to HierarchyDynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.