phi_13_bounds
plain-language theorem explainer
The bound shows phi to the thirteenth power lies below 550, capping the upper end of phi-derived mass-to-light ratios for galaxy clusters. Astrophysicists checking recognition-cost models of stellar assembly cite it to verify that theoretical M/L values remain inside the observed 100-550 window. The proof reduces the claim via unfolding, a numerical bound on phi, monotonicity of powers, and direct computation chained by transitivity.
Claim. $phi^{13} < 550$ where $phi$ is the golden ratio and $phi^n$ denotes the recognition-cost candidate for the mass-to-light ratio at integer tier $n$.
background
The Mass-to-Light module resolves the objection that observed M/L ratios (100-500 solar units) are external inputs by deriving them from recognition-weighted stellar assembly on the phi-ladder. The definition phi_power n equals phi raised to n and supplies the discrete candidates that match the observed band. This setting rests on the ledger factorization that fixes recognition costs and on the multiplicative recognizer cost that weights mass versus light events.
proof idea
The tactic proof unfolds phi_power to reach phi^13 < 550. It establishes phi < 1.62 by norm_num together with a square-root comparison on sqrt(5), applies the power inequality to obtain phi^13 < 1.62^13, evaluates the right-hand side by norm_num, and closes with lt_trans from ArithmeticFromLogic.
why it matters
The result supplies the upper endpoint for the interval used in ml_consistent_with_observation, which asserts an n between 10 and 13 such that phi^n lies inside 100-550 and thereby confirms the derived ratio matches data. It likewise supports ml_is_derived_not_input by showing the ratio is generated from cycleLength and phi_power rather than inserted externally. In the framework this step instantiates the phi-ladder for dimensionless ratios, aligning with the eight-tick octave and the algebraic derivation of alpha.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.