closure_forces_golden_equation
plain-language theorem explainer
A geometric scale sequence closed under additive ledger composition must satisfy the ratio equation r² = r + 1. Researchers tracing the T5 to T6 bridge in Recognition Science cite this step to obtain the self-similar fixed point from the closure axiom. The proof unfolds the isClosed predicate on the sequence, simplifies the resulting power identities, and rearranges via linear arithmetic.
Claim. Let S be a geometric scale sequence with ratio r > 0 and r ≠ 1. If S is closed under additive ledger composition, then r² = r + 1.
background
GeometricScaleSequence is the structure holding a positive real ratio r ≠ 1 together with the scales r^n for n ∈ ℕ. ledgerCompose is the binary operation that adds two scales, reflecting the additive total recognition work measured by the J-cost J(x) = ½(x + 1/x) - 1. The predicate isClosed requires that the composition of the scales at positions 0 and 1 equals the scale at position 2, which expands to the relation 1 + r = r².
proof idea
The term proof first unfolds isClosed, ledgerCompose and scale at the hypothesis to obtain r^0 + r^1 = r². It then applies simp only [pow_zero, pow_one] to reduce the powers, after which linarith rearranges the equality into the target form r² = r + 1.
why it matters
This theorem converts the closure axiom into the golden equation and is invoked directly by hierarchy_forces_golden_equation to recover the Fibonacci relation from a minimal hierarchy and by self_similar_forces_golden_constraint to enforce the golden constraint on self-similar objects. It occupies the T5–T6 position in the forcing chain, where J-uniqueness yields the self-similar fixed point φ. The derivation of closure itself remains in HierarchyDynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Golden-ratio exponent fixes a gravity kernel, then meets 147 galaxies
"Self-similarity: a geometric scale sequence 1, s, s², ... closed under additive ledger composition satisfies 1+s = s², whose unique positive root is s = φ"