phi_from_fibonacci_ratio
plain-language theorem explainer
Positive reals r obeying r squared equals r plus one equal the golden ratio phi. Workers deriving the phi-ladder for J-cost hierarchies in Recognition Science cite this when closing self-similarity steps. The argument forms the quadratic discriminant, applies a zero-product case split, and discards the negative root by sign analysis and linear arithmetic.
Claim. If $r > 0$ is a real number satisfying $r^2 = r + 1$, then $r = phi$.
background
The Local Cache Forcing module shows J-cost minimization on connected graphs forces hierarchical local caching and closes Gap G1 in the brain holography derivation. J-cost is the derived cost induced by a multiplicative recognizer comparator on positive ratios. The theorem identifies the positive root of the Fibonacci recurrence with phi, the self-similar fixed point forced at T6 of the unified forcing chain.
proof idea
The proof verifies sqrt(5) squared equals 5 and sqrt(5) exceeds 1. It forms the product (r minus (1 plus sqrt(5))/2) times (r minus (1 minus sqrt(5))/2) equals zero via nlinarith. The mul_eq_zero case split yields the positive root matching the phi definition by linarith, while the negative root produces an exfalso via sign comparison.
why it matters
This result supplies the fourth conjunct of the local_cache_forcing_certificate, which feeds directly into brain_holography_fully_forced. It realizes the T6 forcing step where phi emerges as the unique positive solution to the recurrence, enabling strict increase of J-cost along the phi-ladder for distance penalties. The proof is complete with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.