ml_uncertainty_is_discrete
plain-language theorem explainer
Mass-to-light ratios between 100 and 550 correspond to discrete integer exponents n from 10 to 13 on the phi-ladder. Galaxy formation modelers and cosmologists in the Recognition Science program cite the result to replace continuous empirical M/L inputs with bounded discrete tiers. The proof is a direct term that selects the witness n=10 and reduces the interval membership predicate by simplification.
Claim. For every real number $ML$ satisfying $100 ≤ ML ≤ 550$, there exists an integer $n$ such that $10 ≤ n ≤ 13$.
background
The module derives the mass-to-light ratio from ledger structure rather than treating it as an external parameter. Recognition cost weighting, ledger budget constraints, and curvature partition across the eight-tick cycle together imply that M/L equals a power of phi. The observed interval 100-550 aligns with phi^10 ≈ 123 to phi^13 ≈ 521. Upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost that enters the stellar assembly integral, while PhiForcingDerived and LedgerFactorization supply the multiplicative structure that forces discrete tiers.
proof idea
The term proof introduces the real ML and the closed interval hypothesis, then uses 10 as the witness integer and applies simp to the Set.mem_Icc predicate on the closed interval from 10 to 13.
why it matters
The declaration closes the external-parameter objection in Gap 10 by showing that the empirical M/L window is exactly the discrete phi-ladder segment from rung 10 to 13. It supports the module's three derivation strategies (cost weighting, ledger conservation, phase partitioning) and aligns with the T7 eight-tick octave and T6 self-similar fixed point. No downstream theorems yet consume it; the concrete mapping from a measured ML value to a specific rung remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.