phi_lt_two
plain-language theorem explainer
The golden ratio φ satisfies φ < 2. Derivations of stellar mass-to-light ratios and electroweak scales cite this bound to close the interval 1 < φ < 2. The proof is a one-line wrapper that applies the tighter estimate φ < 1.62 via linear arithmetic.
Claim. The golden ratio satisfies $φ < 2$.
background
The Mathematics.Euler module derives Euler's number from φ-summations in Recognition Science. Here φ denotes the golden ratio (1 + √5)/2, the self-similar fixed point forced by the J-cost equation. This lemma supplies the upper bound needed to normalize quantities on the phi-ladder and close intervals used in mass formulas and probability normalizations.
proof idea
The proof is a one-line wrapper that invokes the lemma phi_lt_onePointSixTwo from Constants and applies linear arithmetic to conclude φ < 2.
why it matters
This bound feeds parent theorems such as ml_matches_stellar_observations, which shows 1 < ml_nucleosynthesis < 5, and vev_phi_window, which pins the electroweak scale inside the same interval. It closes the upper end of the φ window required by the eight-tick octave and phi-ladder constructions. The module explores connections to e but leaves open any direct algebraic relation between the two constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.