phi_bounds
The golden ratio satisfies the tight numerical bounds 1.618033 < phi < 1.618034. Researchers deriving mass ladders and gap residues in Recognition Science cite this to control precision in numerical evaluations of structural residues. The proof first bounds sqrt(5) between 2.236066 and 2.236068 via direct squaring comparisons, then applies linear arithmetic to obtain the corresponding bounds on (1 + sqrt(5))/2.
claimLet $phi = (1 + sqrt(5))/2$. Then $1.618033 < phi < 1.618034$.
background
The module verifies algebraic and analytic properties of the structural residue gap(Z) = log(1 + Z/phi) / log phi, which functions as the zero-parameter Recognition-side residue f^Rec in the mass framework. This supplies Lean-checked behavior for gap without reliance on external renormalization kernels. Upstream results include the coarser bound 1 < phi < 2 from Astrophysics.MassToLight.phi_bounds, which this declaration tightens for downstream numerical work.
proof idea
The tactic proof first establishes sqrt(5) > 2.236066 by verifying (2.236066)^2 < 5 and applying sqrt_lt_sqrt, then sqrt(5) < 2.236068 by verifying 5 < (2.236068)^2. It next uses linarith on the linear expressions 1 + sqrt(5) to bound (1 + sqrt(5))/2 from below by 1.618033 and from above by 1.618034, followed by unfolding the definition of phi.
why it matters in Recognition Science
This supplies the precise numerical control on phi required by downstream gap bounds such as gap_24_bounds, gap_276_bounds, and gap_1332_bounds. It pins the value of the self-similar fixed point for the phi-ladder in mass formulas, consistent with the forcing chain step that forces phi. The declaration closes a numerical interface used across ElectronMass.Necessity and RSBridge.GapProperties without introducing new hypotheses.
scope and limits
- Does not prove irrationality or continued-fraction properties of phi.
- Does not derive phi from the Recognition Composition Law or the functional equation.
- Does not bound gap(Z) itself or any mass formula.
- Does not address convergence of the phi-ladder or higher-order corrections.
Lean usage
have hphi := phi_boundsformal statement (Lean)
292lemma phi_bounds : (1.618033 : ℝ) < phi ∧ phi < (1.618034 : ℝ) := by
proof body
Tactic-mode proof.
293 -- φ = (1 + √5)/2
294 -- We need: 2.236066 < √5 < 2.236068
295 have sqrt5_lower : (2.236066 : ℝ) < Real.sqrt 5 := by
296 have h : (2.236066 : ℝ)^2 < 5 := by norm_num
297 have h_pos : (0 : ℝ) ≤ 2.236066 := by norm_num
298 rw [← Real.sqrt_sq h_pos]
299 exact Real.sqrt_lt_sqrt (by norm_num) h
300 have sqrt5_upper : Real.sqrt 5 < (2.236068 : ℝ) := by
301 have h : (5 : ℝ) < (2.236068)^2 := by norm_num
302 have h_pos : (0 : ℝ) ≤ 2.236068 := by norm_num
303 rw [← Real.sqrt_sq h_pos]
304 exact Real.sqrt_lt_sqrt (by positivity) h
305 constructor
306 · -- Lower bound
307 have h : (1.618033 : ℝ) < (1 + Real.sqrt 5) / 2 := by
308 have : (1 : ℝ) + 2.236066 < 1 + Real.sqrt 5 := by linarith
309 linarith
310 simp only [phi]
311 exact h
312 · -- Upper bound
313 have h : (1 + Real.sqrt 5) / 2 < (1.618034 : ℝ) := by
314 have : (1 : ℝ) + Real.sqrt 5 < 1 + 2.236068 := by linarith
315 linarith
316 simp only [phi]
317 exact h
318
319/-- Hypothesis: log(1.618033) > 0.481211 (verified externally via Taylor expansion) -/