phi_worst_approximable_core
plain-language theorem explainer
The theorem asserts that the golden ratio φ is irrational and equals its own continued fraction iteration. Researchers in Diophantine approximation and Recognition Science cost models cite it to anchor Hurwitz optimality bounds on rational approximations. The proof is a direct term-mode conjunction of the irrationality result and the fixed-point lemma for the iteration map.
Claim. Let φ = (1 + √5)/2. Then φ is irrational and the continued fraction iteration map satisfies cfracIteration(φ) = φ.
background
The module treats continued fractions as sequential J-cost optimization on the positive reals. The J-cost functional J(x) = ½(x + x⁻¹) − 1 is strictly convex with unique minimum at x = 1; its self-similar fixed point is the unique positive solution to x = 1 + 1/x, which is φ. A continued fraction step chooses the ratio minimizing local J-cost subject to nesting, and infinite iteration converges to φ because it is the attractor of the recursion x ↦ 1 + 1/x (from T5 and T6 in the forcing chain). Upstream, phi_irrational records that φ equals Mathlib's goldenRatio and is therefore irrational via the irrationality of √5.
proof idea
The proof is a one-line term wrapper that applies the conjunction of phi_irrational (establishing Irrational phi) and phi_is_cfrac_fixed_point (establishing cfracIteration phi = phi).
why it matters
This core supplies the Hurwitz-optimality direction for the Ramanujan bridge: φ resists rational approximation more tightly than any other irrational, so its J-cost optimization converges slowest. It directly instantiates T6 (phi forced as self-similar fixed point) and supports the claim that all partial quotients equal 1 yields the minimal per-level cost J(φ) ≈ 0.118. No downstream uses are recorded yet; the fact closes the scaffolding between the continued-fraction fixed-point property and the broader Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.