phi_from_fibonacci_ratio
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not prove existence of phi from first principles.
- Does not apply when r is non-positive.
- Does not address approximate or numerical roots.
- Does not derive J-cost monotonicity without sibling lemmas.
Lean usage
example (r : ℝ) (hr : 0 < r) (hf : r ^ 2 = r + 1) : r = phi := phi_from_fibonacci_ratio r hr hfformal statement (Lean)
119theorem phi_from_fibonacci_ratio (r : ℝ) (hr_pos : 0 < r)
120 (hfib : r ^ 2 = r + 1) : r = phi := by
proof body
Tactic-mode proof.
121 have hsq5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 5)
122 have hsqrt5_gt1 : Real.sqrt 5 > 1 := by
123 have : Real.sqrt 5 > Real.sqrt 1 :=
124 Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1 : ℝ) < 5)
125 simpa [Real.sqrt_one] using this
126 have hdisc : (r - (1 + Real.sqrt 5) / 2) * (r - (1 - Real.sqrt 5) / 2) = 0 := by
127 nlinarith [hsq5]
128 rcases mul_eq_zero.mp hdisc with h | h
129 · unfold phi; linarith
130 · exfalso
131 have h_neg : (1 - Real.sqrt 5) / 2 < 0 := by linarith
132 linarith
133
134/-! ## Part 6: At Global Minimum → Holographic -/
135
136/-- At the J-cost global minimum (all edge costs zero), the allocation is
137 holographic: every vertex has the same field value. -/