sequential_optimization_forces_phi_strong
plain-language theorem explainer
Any positive real fixed point of the map r ↦ 1 + 1/r equals the golden ratio φ. Researchers modeling continued fractions or sequential J-cost minimization in Recognition Science cite this uniqueness result to justify convergence of the infinite iteration. The tactic proof derives the quadratic r² = r + 1, invokes the identity φ² = φ + 1, factors the difference of roots, and applies positivity to discard the extraneous factor.
Claim. Let $r > 0$ be a real number satisfying the fixed-point equation $r = 1 + 1/r$. Then $r$ equals the golden ratio $φ$.
background
The module treats continued fractions as sequential J-cost optimization on the positive reals. The J-cost functional is defined by $J(x) = ½(x + x^{-1}) - 1$, which is strictly convex with unique minimum at $x=1$. A continued fraction corresponds to a chain of local ratio choices; self-similarity forces the scale ratio $r$ to satisfy the same recurrence at every level, yielding the fixed-point equation $r = 1 + 1/r$ whose positive solution is $φ$ (T6). Upstream lemma phi_sq_eq states the key identity $φ² = φ + 1$ (from the defining equation $x² - x - 1 = 0$). Upstream lemma one_lt_phi asserts $1 < φ$.
proof idea
The tactic proof introduces the hypotheses, derives $r² = r + 1$ by field simplification on the fixed-point equation, recalls phi_sq_eq to obtain the companion identity for $φ$, applies nlinarith to produce the factorization $(r - φ)(r + φ - 1) = 0$, uses linarith together with one_lt_phi to show the second factor is positive, invokes mul_eq_zero to conclude the first factor vanishes, and finishes with linarith.
why it matters
The result supplies the uniqueness half of the self-similar fixed-point argument that identifies $φ$ as the ground state of J-cost minimization for continued fractions. It directly instantiates T6 (phi forced as the self-similar fixed point) from the UnifiedForcingChain and supports the RamanujanBridge claim that deeply nested continued fractions compute the minimum-J-cost geodesic. No downstream uses are recorded, leaving open whether the lemma will be invoked inside the full RCL or phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.