phi_gt_one
plain-language theorem explainer
The golden ratio φ satisfies φ > 1. Derivations of mass-to-light ratios as integer powers of φ cite this base fact to guarantee that positive exponents produce values exceeding unity and to anchor the φ-ladder bounds. The short tactic proof unfolds the definition of φ as (1 + sqrt(5))/2, invokes the monotonicity of the square root to show sqrt(5) > 1, and finishes with linear arithmetic.
Claim. Let φ = (1 + √5)/2 denote the golden ratio. Then φ > 1.
background
The MassToLight module derives candidate M/L ratios from recognition-weighted stellar assembly, showing that observed values 100-500 arise as φ^10 to φ^13 rather than as external parameters. φ itself is imported from Constants as the unique positive fixed point of the Recognition Composition Law, satisfying the quadratic that forces self-similarity in the eight-tick cycle.
proof idea
The proof is a short tactic sequence. It unfolds the definition of phi, proves sqrt(5) > 1 by rewriting sqrt(1) and applying sqrt_lt_sqrt with norm_num witnesses, then closes with linarith.
why it matters
This lemma supplies the elementary inequality required by the geometric bounds helpers (phi_gt_1_6, phi_lt_1_7, phi_10_bounds) that convert the φ-ladder into concrete M/L predictions. It sits inside the Gap 10 resolution that replaces empirical M/L input with algebraic output from the ledger topology and the T6 fixed-point construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.