phi_forcing_complete
plain-language theorem explainer
The golden ratio is the unique positive real r ≠ 1 satisfying the closure equation 1 + r = r² for geometric scale sequences under additive ledger composition. Recognition Science derivations of the self-similar fixed point cite this result to close the T5–T6 bridge. The proof rewrites the hypothesis as a quadratic, factors the difference against the known phi identity, and discards the negative root by positivity.
Claim. Let $r > 0$ with $r ≠ 1$. If $1 + r = r^2$, then $r = φ$ where $φ = (1 + √5)/2$.
background
The module derives the scale ratio from three axioms: scales form the geometric sequence {1, r, r², …}, ledger composition of independent events is additive because total J-cost is additive, and the sequence is closed so that the composed scale 1 + r must equal the next term r². J-cost is defined as J(x) = Cost.Jcost x and obeys the Recognition Composition Law specialized to J(ab) + J(a/b) = 2 J(a) J(b) + 2 J(a) + 2 J(b). The local setting is the T5→T6 bridge: given closure, uniqueness of the fixed point follows; the deeper derivation of closure itself appears in HierarchyDynamics via uniform scaling and local binary recurrence.
proof idea
The tactic proof introduces r, the positivity and non-equality hypotheses, and the closure equation. It rewrites the closure as r² = r + 1, recalls the upstream identity phi² = phi + 1, and forms the factored difference (r − phi)(r + phi − 1) = 0 by ring_nf and nlinarith. Application of mul_eq_zero splits into cases; the first yields r = phi by linarith, while the second produces r = 1 − phi, which is shown negative by one_lt_phi and linarith.
why it matters
This theorem supplies the uniqueness step that forces phi as the self-similar fixed point once closure is granted, completing the T5 J-uniqueness to T6 phi-forcing link in the eight-tick octave construction. It feeds the scale sequence used in LargeScaleStructureFromRS and the phi-ladder mass formula. The parent derivation of the closure condition itself (Fibonacci recurrence from zero-parameter locality) is stated in HierarchyDynamics; the present result closes the algebraic gap without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.