phi_10_bounds
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.