phi_lt_1_7
plain-language theorem explainer
The golden ratio φ satisfies φ < 1.7. Mass-to-light derivations cite the bound to confirm that φ^10 ≈ 123 and φ^13 ≈ 521 lie inside observed galaxy cluster ratios of 100-500. The tactic proof unfolds the definition of φ, establishes sqrt(5) < 2.4 via square-root monotonicity, and closes with linear arithmetic.
Claim. Let φ = (1 + √5)/2 be the golden ratio. Then φ < 1.7.
background
The MassToLight module derives the mass-to-light ratio from recognition cost weighting over stellar mass functions, ledger budget constraints, and curvature partitions in the eight-tick cycle. It shows that observed M/L values between 100 and 500 equal φ^n for integer n in 10 to 13, resolving the objection that M/L is an external empirical input rather than a first-principles output. The golden ratio φ arises as the self-similar fixed point in the Recognition Science forcing chain.
proof idea
Unfold the definition of phi. Apply norm_num to the resulting numerical inequality. Introduce the auxiliary claim Real.sqrt 5 < 2.4 by rewriting the square of 2.4 and invoking Real.sqrt_lt_sqrt on the positive terms. Finish the main goal with linarith.
why it matters
The lemma supplies the upper bound required by ml_is_phi_power, which asserts existence of n in 10..13 such that observed M/L lies within 400 of φ^n. It also populates the coarse interval in phi_bounds_stub. In the framework φ is the self-similar fixed point (T6) whose powers generate the mass ladder and the M/L ratio in the Gap 10 derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.