phi_lt_16180340
plain-language theorem explainer
This supplies the concrete upper bound φ < 1.6180340 for the golden ratio inside Recognition Science constants. Numerics code for phi-powers, log bounds, and w8 interval arithmetic cites it to keep error propagation under control. The proof verifies 5 < (2.236068)^2 by norm_num, deduces sqrt(5) < 2.236068 via Real.sqrt_lt, unfolds the definition of phi, and closes with linarith.
Claim. The golden ratio satisfies $φ < 1.6180340$, where $φ = (1 + √5)/2$.
background
The W8Bounds module supplies rigorous decimal bounds on φ and √2 to certify the gap weight w8 = (348 + 210√2 - (204 + 130√2)φ)/7 near 2.490569. This theorem gives the upper half of the φ interval used throughout the numerics layer for mass and alpha calculations.
proof idea
The tactic proof first uses norm_num to obtain 0 ≤ 5, 0 ≤ 2.236068, and 5 < (2.236068)^2. It applies Real.sqrt_lt to conclude sqrt(5) < 2.236068. After unfolding Constants.phi, linarith assembles the target inequality.
why it matters
This bound is invoked by phi_in_phiIntervalTight, phi_pow51_lt, phi_quarter_lt, and phi_tight_bounds inside PhiBounds, and by log_phi_lt_0483 inside AlphaBounds and Log. It supplies the numerical anchor needed to bound w8 and to place alpha^{-1} inside (137.030, 137.039). The result supports the eight-tick octave and the derivation of D = 3 by keeping all phi-ladder calculations inside verified intervals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.