H_MLUncertaintyIsDiscrete
plain-language theorem explainer
The declaration encodes the scaffold hypothesis that mass-to-light ratios ML in the interval 100 to 550 must coincide with integer powers of phi from n=10 to n=13. Galaxy-cluster modelers working inside the recognition ledger would invoke it when replacing empirical M/L inputs with phi-ladder outputs. The definition is a direct one-line encoding of the discrete-uncertainty claim, marked as scaffold pending the instability proof for non-power values.
Claim. The hypothesis asserts that if the mass-to-light ratio satisfies $100 ≤ ML ≤ 550$, then there exists an integer $n$ with $10 ≤ n ≤ 13$ such that $ML = φ^n$, where $φ$ denotes the golden-ratio fixed point.
background
The Mass-to-Light module derives the M/L ratio from recognition-weighted stellar assembly on the ledger, showing that the ratio must lie on the phi-ladder rather than taking continuous values. The auxiliary definition phi_power(n) simply returns $φ^n$ and supplies the candidate discrete values $φ^{10} ≈ 123$ to $φ^{13} ≈ 521$ that bracket the observed astronomical range. The module's local setting treats M/L as an output of J-cost topology and the eight-tick cycle partition between mass accumulation and photon emission phases.
proof idea
The declaration is a definition that directly transcribes the implication 100 ≤ ML ∧ ML ≤ 550 → ∃ n ∈ Icc 10 13, ML = phi_power n. It performs no lemma applications or tactic steps; the body is a literal statement of the scaffold hypothesis with an inline comment marking the missing instability argument.
why it matters
This scaffold closes the empirical-input objection in Gap 10 by asserting that observed M/L values are forced onto the phi-ladder. It supports the larger claim that all dimensionless ratios in Recognition Science are algebraic in phi, consistent with the J-uniqueness relation and the self-similar fixed point. The open task it flags is a formal proof that non-power M/L values are unstable under the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.