phi_bounds
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.