phi_10_bounds
phi_10_bounds shows that the golden ratio to the tenth power exceeds 100, supplying the lower edge of the mass-to-light interval derived from recognition costs. Galaxy-cluster analysts cite it to verify that phi-powered M/L values sit inside the observed 100-550 window. The proof unfolds the power definition, applies the phi > 1.6 lemma, raises both sides to the tenth power, and chains the numerical comparison 1.6^10 > 100 through transitivity.
claim$phi^{10} > 100$, where $phi$ is the golden ratio and the exponent is an integer rung on the recognition ladder.
background
The MassToLight module derives galaxy mass-to-light ratios from the recognition ledger rather than from external data. phi_power n is the definition phi^n; it supplies candidate M/L values on the phi-ladder. The supporting lemma phi_gt_1_6 states phi > 1.6 and is proved by unfolding phi and comparing square roots. Module documentation frames the result as part of the resolution that M/L emerges from recognition-weighted stellar assembly and the eight-tick cycle partition, matching the observed range 100-550 via powers 10 to 13.
proof idea
The tactic proof unfolds phi_power, obtains the hypothesis phi > 1.6 from the sibling lemma phi_gt_1_6, applies pow_lt_pow_left to produce phi^10 > 1.6^10, invokes norm_num to establish 1.6^10 > 100, and finishes with gt_of_gt_of_gt to chain the two inequalities.
why it matters in Recognition Science
The bound is invoked by ml_consistent_with_observation and ml_is_derived_not_input to witness that an integer n between 10 and 13 satisfies 100 < phi^n < 550. It thereby completes the argument that M/L is an output of the Recognition framework (phi fixed point, phi-ladder mass formula, RCL) rather than an empirical input. The result sits inside the Gap 10 derivation that closes the objection about external parameters.
scope and limits
- Does not establish an exact numerical M/L for any specific galaxy or cluster.
- Does not prove the companion upper bound phi^13 < 550.
- Does not treat non-integer exponents or continuous mass distributions.
- Does not derive the underlying phi value itself.
formal statement (Lean)
99theorem phi_10_bounds : phi_power 10 > 100 := by
proof body
Tactic-mode proof.
100 unfold phi_power
101 have h : phi > 1.6 := phi_gt_1_6
102 have h10 : phi ^ 10 > 1.6 ^ 10 := pow_lt_pow_left h (by norm_num) (by norm_num)
103 have : (1.6 : ℝ) ^ 10 > 100 := by norm_num
104 exact gt_of_gt_of_gt h10 this
105
106/-- φ¹³ < 550. -/