phi_lt_two
plain-language theorem explainer
Recognition Science calculations of stellar mass-to-light ratios and electroweak vacuum expectation values invoke the inequality φ < 2 to bound φ-powered quantities within observational windows. Cosmologists and condensed-matter physicists reference it when closing interval arguments for the golden ratio in tiered structures. The tactic proof establishes the bound by showing √5 < 3 through comparison with √9, deriving 1 + √5 < 4, dividing by 2, and finishing with linear arithmetic after unfolding the definition of φ.
Claim. The golden ratio satisfies $φ < 2$, where $φ = (1 + √5)/2$.
background
The Constants module introduces φ as the golden ratio, the unique positive root of x² = x + 1. Recognition Science identifies this root as the self-similar fixed point forced by the J-uniqueness condition and the fixed-point equation in the T0-to-T8 chain. The bound is paired with the companion result φ > 1 to locate φ inside (1, 2), the interval required for realistic exponents on the φ-ladder mass formula and coupling constants.
proof idea
The proof first establishes √5 < 3 by comparing 5 < 9 and invoking monotonicity of the square-root function, then shows 1 + √5 < 4 by linear arithmetic. Division by 2 produces the target inequality for (1 + √5)/2. After unfolding the definition of φ, linarith closes the goal.
why it matters
The bound is invoked by ml_matches_stellar_observations to verify that the nucleosynthesis-derived M/L ratio lies between 1 and 5, matching observed stellar populations. It likewise appears in vev_phi_window to constrain the electroweak scale and in high_tc_superconductivity_structure to establish the structural interval for high-Tc materials. Within the framework it supports the phi-ladder mass formula and the eight-tick octave by guaranteeing that φ generates physically plausible exponents in the interval (1, 2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.