phi_gt_one
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.
claimLet φ = (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 in Recognition Science
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.
scope and limits
- Does not prove irrationality of φ.
- Does not supply numerical approximations or decimal bounds.
- Does not address specific exponents or M/L applications.
- Does not rely on any upstream lemmas from the module.
formal statement (Lean)
64lemma phi_gt_one : phi > 1 := by
proof body
Tactic-mode proof.
65 unfold phi
66 have : Real.sqrt 5 > 1 := by
67 rw [← Real.sqrt_one]
68 exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
69 linarith
70