phi_gt_1_6
plain-language theorem explainer
The golden ratio exceeds 1.6. Derivations of mass-to-light ratios cite this bound to show that the tenth power of the golden ratio exceeds 100 and lies in the observed range. The proof unfolds the closed-form definition, reduces the claim via norm_num, establishes an auxiliary square-root inequality, and closes with linarith.
Claim. $φ > 1.6$ where $φ = (1 + √5)/2$ denotes the golden ratio.
background
The MassToLight module derives the mass-to-light ratio from recognition cost weighting on stellar mass functions, showing that the ratio equals a power of the golden ratio between 10 and 13. The golden ratio enters as the self-similar fixed point of the forcing chain. This lemma supplies the numerical lower bound required for the subsequent power estimates.
proof idea
The tactic proof unfolds the definition of phi, applies norm_num, proves the auxiliary claim Real.sqrt 5 > 2.2 by rewriting with sqrt_sq and invoking Real.sqrt_lt_sqrt, then finishes with linarith.
why it matters
The bound is invoked by ml_is_phi_power to place observed M/L values inside the interval φ^10 to φ^13 and by phi_10_bounds to obtain the concrete inequality φ^10 > 100. It therefore anchors the phi-ladder used for mass formulas and the recognition-weighted stellar assembly argument in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.