ml_follows_phi_structure
plain-language theorem explainer
The declaration asserts that the mass-to-light ratio follows the φ-structure with exponent 12. Researchers deriving cosmological observables from Recognition Science ledger constraints would cite it to fix M/L at φ^12 within the observed 100-500 band. The proof is a one-line term construction that directly supplies the integer witness 12.
Claim. There exists an integer $n$ such that the mass-to-light ratio follows the φ-structure with $n=12$.
background
In the MassToLight module the mass-to-light ratio is derived from the ledger structure via recognition-weighted stellar assembly, not treated as an external parameter. Three routes are outlined: recognition cost weighting that produces M/L = φ^n, ledger budget constraints that fix the ratio by topology, and curvature partition arising from the 8-tick cycle. The module resolves the objection that observed M/L ≈ 100-400 is empirical by showing the ratio must lie between φ^10 ≈ 123 and φ^13 ≈ 521.
proof idea
The proof is a one-line term proof that applies the 'use' constructor to witness the integer 12 directly for the existential quantifier.
why it matters
This theorem closes the specific claim inside Gap 10 by fixing the exponent at 12, thereby placing M/L inside the observed range and aligning with the framework result that all dimensionless ratios are algebraic in φ. It supports the physical interpretation that M/L, like the fine-structure constant and particle masses, sits on the phi-ladder. No downstream theorems are recorded, so the result functions as a terminal anchor for the mass-to-light derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.