ml_is_derived_not_input
plain-language theorem explainer
The declaration exhibits an explicit map that produces the mass-to-light ratio by feeding the recognition cycle length into the phi-power function, with the resulting value lying inside the observed interval 100-550. Galaxy-cluster modelers working inside Recognition Science would cite the result to rebut the charge that M/L is an external parameter. The term proof simply constructs the map as phi_power, matches the equality by reflexivity, and checks the bounds at exponent 10 by direct appeal to the supplied inequalities.
Claim. There exists a map $d : ℕ → (ℤ → ℝ)$ such that $d(8)$ coincides with the function $n ↦ ϕ^n$ and there exists an integer $n$ for which $100 < d(8)(n) < 550$.
background
The module treats the mass-to-light ratio as an output of the recognition ledger rather than an observed input. cycleLength counts the eight events that constitute one full recognition cycle; phi_power raises the golden ratio to an integer exponent. Upstream theorems establish the concrete bounds phi^10 > 100 and phi^13 < 550 by using the inequality phi > 1.6 together with monotonicity of the power function. The local setting is the explicit resolution of the objection that M/L ≈ 100-400 M⊙/L⊙ must be inserted by hand; the module instead derives it from recognition-cost weighting, ledger-budget conservation, and the phase partition inside the eight-tick cycle.
proof idea
The term-mode proof begins by supplying the concrete function fun _ n => phi_power n. Reflexivity discharges the equality conjunct. The existential is witnessed by the integer 10; the lower bound is taken directly from the phi_10_bounds theorem while the upper bound follows by transitivity of the strict inequality phi^10 < phi^13 (obtained via zpow_lt_zpow_of_one_lt) with the phi_13_bounds theorem.
why it matters
The result removes the mass-to-light ratio from the list of free parameters by exhibiting it as a direct consequence of the phi-ladder evaluated on the cycle length. It therefore supports the larger claim that all dimensionless cosmological ratios arise algebraically from the J-cost topology and the eight-tick octave. The parent structure is the module-level argument that M/L follows from recognition-weighted stellar assembly and curvature partition; the scaffold comment immediately below flags the remaining open task of proving that non-phi-power values are unstable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.