phi_gt_1_6
plain-language theorem explainer
Lower bound 1.6 < φ holds for the golden ratio appearing in Recognition Science constants. Workers on mass-to-light derivations reference it when establishing that φ^10 exceeds 100. The argument rewrites the target inequality, applies a positivity-preserving division rule, and finishes via linarith on the auxiliary sqrt(5) > 2.2 fact.
Claim. $1.6 < phi$ where $phi = (1 + sqrt(5))/2$ is the golden ratio constant from the CPM bundle.
background
The Support.PhiApprox module supplies numerical bounds for the golden ratio φ that arises as the self-similar fixed point forced by the Recognition Science chain. Constants is the abstract bundle of CPM constants that packages φ together with Knet, Cproj, Ceng and Cdisp. The upstream lemma sqrt5_gt_2_2 states that 2.2 < sqrt(5) and is proved by comparing squares then invoking monotonicity of the square root.
proof idea
The tactic proof unfolds Constants.phi, rewrites 1.6 as (1 + 2.2)/2 by norm_num, applies div_lt_div_of_pos_right with a positive denominator, and closes the resulting inequality by linarith citing sqrt5_gt_2_2.
why it matters
This bound feeds the parent theorems ml_is_phi_power and phi_10_bounds in the MassToLight derivations, which show that observed mass-to-light ratios lie near integer powers of φ between 10 and 13. It supplies the lower half of the phi_bounds_stub used by downstream numerics. In the framework it anchors the T6 self-similar fixed point and enables the eight-tick octave scaling for mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.