phi_from_fibonacci_ratio
plain-language theorem explainer
Any positive real r satisfying the quadratic r² = r + 1 equals the golden ratio φ. Researchers closing the local cache forcing argument in the GCIC brain holography derivation cite this lemma to identify the self-similar ratio. The tactic proof computes the discriminant via nlinarith, splits cases with mul_eq_zero, matches the positive root to φ by linarith, and obtains exfalso on the negative root.
Claim. If $r > 0$ and $r^2 = r + 1$, then $r = phi$.
background
The module establishes that J-cost minimization on connected graphs forces hierarchical local caching, closing Gap G1 toward brain holography. This theorem supplies the identification of the positive root of the Fibonacci quadratic with φ, which anchors the phi-ladder in subsequent cost comparisons. The local setting is J-cost minimization on graphs, with upstream reliance on the ring property that a product equals zero only if a factor is zero (mul_eq_zero from IntegersFromLogic).
proof idea
The proof first records sqrt(5)^2 = 5 and sqrt(5) > 1. It forms the factored discriminant (r - (1 + sqrt(5))/2) * (r - (1 - sqrt(5))/2) = 0 by nlinarith on the given equation. Cases via mul_eq_zero.mp: the first unfolds phi and concludes by linarith; the second derives a contradiction by showing the negative root is less than zero.
why it matters
The result is invoked inside local_cache_forcing_certificate and brain_holography_fully_forced to complete the conjunction that includes strict monotonicity of Jcost on phi powers together with the Fibonacci-to-phi step. It supplies the explicit T6 forcing of phi as self-similar fixed point within the UnifiedForcingChain. No scaffolding remains for this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.