closed_ratio_is_phi
plain-language theorem explainer
The theorem states that any closed geometric scale sequence has ratio exactly the golden ratio φ. Researchers deriving scale hierarchies from closure axioms in Recognition Science cite it to fix the unique positive self-similar ratio. The proof first invokes closure_forces_golden_equation to obtain the quadratic r² = r + 1, matches it to phi_sq_eq, factors the difference, and discards the negative root via one_lt_phi and ratio positivity.
Claim. Let $S$ be a geometric scale sequence with ratio $r > 0$, $r ≠ 1$. If $S$ is closed under additive ledger composition (so that the composition of scales 1 and $r$ lies in the sequence and equals $r^2$), then $r = φ = (1 + √5)/2$.
background
A GeometricScaleSequence is a structure carrying a ratio $r ∈ ℝ$ with $0 < r ≠ 1$ together with the powers $r^n$ as its scales. The module derives the closure condition $r^2 = r + 1$ from three axioms: discrete geometric scales, additive ledger composition (J-cost is additive), and closure under that composition. The upstream lemma closure_forces_golden_equation supplies exactly this quadratic from the axioms. The constants module supplies the companion identity $φ^2 = φ + 1$ and the strict inequality $1 < φ$.
proof idea
Apply closure_forces_golden_equation to obtain $r^2 = r + 1$. Invoke phi_sq_eq to obtain the same equation for φ. Form the difference polynomial $(r - φ)(r + φ - 1) = 0$ by ring_nf and nlinarith. Case analysis on mul_eq_zero yields either $r = φ$ or $r = 1 - φ < 0$. The second case contradicts ratio_pos, so $r = φ$.
why it matters
This result completes the T5-to-T6 step in the forcing chain: given closure, the unique positive fixed point is forced to be φ. It is invoked directly by hierarchy_forces_phi (MinimalHierarchy) and hierarchy_emergence_forces_phi (UniformScaleLadder with additive closure). The module doc positions it as the bridge between the closure axiom and the self-similar ratio required for the eight-tick octave and D = 3.
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 = φ"