phi_lt_two
plain-language theorem explainer
The theorem establishes that the golden ratio φ is strictly less than 2. Researchers deriving mass-to-light ratios from nucleosynthesis tiers or pinning electroweak scales to the phi interval would cite this bound to close interval estimates. The proof unfolds the definition of φ, shows sqrt(5) < 3 by direct comparison to sqrt(9) = 3, and finishes with linear arithmetic.
Claim. $φ < 2$, where $φ = (1 + √5)/2$ is the golden ratio forced by self-similarity in a discrete ledger with J-cost.
background
The Phi Forcing module derives the golden ratio as the unique positive scale ratio satisfying the self-similarity condition under J-cost in a discrete ledger. Self-similar scales obey x² = x + 1 because J(x) must equal J(1) = 0 while x ≠ 1, yielding φ as the only solution greater than 1. The bound φ < 2 is a basic numerical fact used to constrain all downstream phi-ladder quantities.
proof idea
The tactic proof unfolds the definition of φ, proves sqrt(5) < 3 by showing it is less than sqrt(9) = 3 via the monotonicity of the square-root function on positives, and concludes with linarith.
why it matters
This bound feeds directly into nucleosynthesis mass-to-light derivations (ml_nucleosynthesis < 5) and the electroweak VEV structural window (1 < φ < 2). It closes the upper end of the scale interval required for the phi-forcing chain, ensuring consistency with the eight-tick octave and observed constants such as alpha inverse near 137. It is invoked in 23 downstream sites across astrophysics and condensed-matter modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.