ml_consistent_with_observation
plain-language theorem explainer
Existence of an integer n between 10 and 13 is shown such that phi to the power n lies strictly between 100 and 550. Galaxy formation researchers cite the result to confirm that the mass-to-light ratio can be read from the phi-ladder without external calibration. The proof exhibits the witness 10, applies the endpoint bounds directly, and chains the inequalities via monotonicity of the power function.
Claim. There exists an integer $n$ with $10leq nleq 13$ such that $100<phi^n<550$.
background
The module treats the mass-to-light ratio as emerging from recognition-weighted stellar assembly on the ledger rather than as an inserted parameter. The definition phi_power n equals phi raised to n supplies the candidate M/L values on the phi-ladder. Upstream phi_10_bounds asserts phi to the tenth exceeds 100 while phi_13_bounds asserts phi to the thirteenth is less than 550; lt_trans supplies the transitivity step from the arithmetic foundation.
proof idea
The tactic proof exhibits the witness 10 and confirms interval membership by simp on Set.mem_Icc. It applies phi_10_bounds for the lower bound. For the upper bound it first proves phi_power 10 < phi_power 13 by zpow_lt_zpow_of_one_lt using phi_gt_one, then invokes lt_trans to reach phi_13_bounds.
why it matters
The theorem closes the Gap 10 treatment by showing that powers of phi inside the interval [10,13] fall inside the observed M/L window 100-550. It supports the module claim that the ratio is algebraic in phi and arises from recognition cost weighting together with the eight-tick cycle. The result aligns with the broader framework in which dimensionless ratios are fixed by the recognition composition law and the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.