phi_lt_1_7
plain-language theorem explainer
The lemma establishes that the Recognition Science constant phi satisfies phi < 1.7. Numerics modules in mass-to-light derivations and bound stubs cite this to control approximation errors on the phi-ladder. The proof reduces the target inequality to a comparison with sqrt(5) < 2.4 via rewriting 1.7 as (1 + 2.4)/2 followed by division and linear arithmetic.
Claim. Let $phi$ be the golden ratio constant from the Constants structure. Then $phi < 1.7$.
background
In the Support.PhiApprox module, coarse numerical bounds are supplied for the golden ratio phi that arises as the self-similar fixed point (T6) in the UnifiedForcingChain. The Constants structure from LawOfExistence bundles this phi together with Knet, Cproj and related parameters. The lemma depends on the sibling sqrt5_lt_2_4, which proves Real.sqrt 5 < 2.4 by comparing squares and applying the monotonicity of sqrt.
proof idea
The tactic proof unfolds Constants.phi, rewrites 1.7 as (1 + 2.4)/2 by norm_num, applies div_lt_div_of_pos_right to reduce the inequality, and closes with linarith using the hypothesis sqrt5_lt_2_4.
why it matters
This bound completes the interval in phi_bounds_stub, which is consumed by ml_is_phi_power to bound errors when mass-to-light ratios are asserted near phi powers. It supports phi-ladder mass formulas and the eight-tick octave while keeping numerics inside the alpha band. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.