phi_lt_two
plain-language theorem explainer
The lemma establishes that the golden ratio φ satisfies φ < 2. Researchers deriving mass-to-light ratios from recognition-weighted stellar assembly would cite this bound to constrain nucleosynthesis tiers and geometric limits. The proof unfolds the definition of φ, shows sqrt(5) < 3 via monotonicity of the square root, and closes with linear arithmetic.
Claim. Let φ denote the golden ratio. Then φ < 2.
background
The module derives the mass-to-light ratio from ledger structure via recognition cost weighting, showing M/L equals a power of φ that matches observed stellar values between 1 and 5. The golden ratio φ is the self-similar fixed point forced in the unified chain. Upstream results supply the same inequality in Constants, PhiForcing, RecognitionEntropy, and Euler modules, each using it to bound entropy comparisons and scale windows.
proof idea
The tactic proof unfolds the definition of phi, proves sqrt(5) < 3 by rewriting sqrt(9) = 3 and applying sqrt_lt_sqrt on positive reals, then finishes with linarith.
why it matters
This bound feeds parent theorems such as ml_matches_stellar_observations and ml_geometric_bounds in NucleosynthesisTiers and ObservabilityLimits, which apply it to verify 1 < M/L < 5 and 1 < M/L < 2. It closes the mass-to-light gap by supplying the upper limit needed for φ^1 ≈ 1.618 to align with the eight-tick cycle and φ-ladder mass formula. The result reinforces that φ lies in (1,2), consistent with T6 self-similarity and the alpha band constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.