phi_gt_1_6
plain-language theorem explainer
The golden ratio satisfies φ > 1.6. Mass-to-light derivations cite the bound to anchor φ^10 > 100 and to match observed galaxy-cluster ratios between 100 and 500. The tactic proof unfolds the definition of φ, normalizes constants, establishes sqrt(5) > 2.2 by monotonicity of the square root, and closes with linear arithmetic.
Claim. $φ > 1.6$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module derives the mass-to-light ratio from recognition cost weighting over stellar mass functions rather than external cluster data. Recognition events are conserved by the ledger topology, so the ratio of mass-bearing to light-emitting events is fixed by the eight-tick cycle and emerges as a power of φ on the phi-ladder. This lemma supplies the concrete numerical lower bound required for the estimates φ^10 > 100 and φ^13 < 521.
proof idea
Unfolds the definition of phi, applies norm_num, introduces the auxiliary claim Real.sqrt 5 > 2.2 by rewriting the target as sqrt(2.2^2) and invoking sqrt_lt_sqrt, then finishes the main goal with linarith.
why it matters
The bound is invoked by phi_10_bounds to obtain φ^10 > 100 and by ml_is_phi_power to place observed M/L ratios on the interval [10,13] of the phi-ladder. It thereby supports the claim that dimensionless ratios in Recognition Science are algebraic in φ, consistent with the self-similar fixed point T6 and the mass formula yardstick · φ^(rung-8+gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.