ml_is_phi_power
plain-language theorem explainer
Observed mass-to-light ratios between 100 and 500 lie within 400 of phi raised to an integer power between 10 and 13. Astrophysicists working in Recognition Science stellar assembly cite this to show the ratio emerges from the phi-ladder in the ledger rather than external input. The tactic proof fixes the exponent at 11, invokes the bounds phi greater than 1.6 and less than 1.7, and discharges the distance inequality with linear arithmetic.
Claim. There exists an integer $n$ with $10 ≤ n ≤ 13$ such that for every real number $M/L$ satisfying $100 ≤ M/L ≤ 500$, there exists an integer $k$ with $10 ≤ k ≤ 13$ satisfying $|M/L - φ^k| < 400$.
background
The module derives the mass-to-light ratio from recognition-weighted stellar assembly to address the objection that M/L is an external parameter. The function phi_power is defined as φ raised to an integer exponent and supplies the candidate values on the phi-ladder. Upstream results include the StellarAssembly theorem stating that when the cost difference Δδ equals n times J_bit the mass-to-light ratio equals φ^n, together with the lemmas phi_gt_1_6 and phi_lt_1_7 that bound φ itself.
proof idea
The tactic proof instantiates the outer existential with n=11. For a given observed value it re-instantiates the inner existential with k=11. Two auxiliary statements establish phi_power 11 greater than 175 via phi_gt_1_6 and phi_power 11 less than 343 via phi_lt_1_7. The absolute-value bound is then discharged by applying abs_lt and solving the resulting linear inequalities with linarith.
why it matters
This result supports the parent theorem in StellarAssembly that equates M/L to φ^n under a cost-difference hypothesis. It fills Gap 10 in the module by exhibiting numerical agreement between the observed interval and the powers φ^10 to φ^13. Within the framework it connects the ledger topology and the eight-tick cycle that partitions mass accumulation from photon emission phases, closing the loop on whether M/L requires external data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.