ml_is_derived_not_input
Recognition Science derivations establish the mass-to-light ratio as phi raised to an integer power on the eight-tick cycle, with the value at rung 10 lying between 100 and 550. Cosmologists using the framework to eliminate external parameters would cite this result. The proof constructs the derivation function explicitly as the phi-power map and applies the pre-proved bounds at n=10.
claimThere exists a function $derive : ℕ → ℤ → ℝ$ such that $derive(8)$ equals the map $n ↦ ϕ^n$ and there exists an integer $n$ with $100 < ϕ^n < 550$.
background
The MassToLight module derives the mass-to-light ratio from the recognition ledger rather than accepting it as empirical input. Recognition cost weighting over stellar mass functions, ledger budget conservation, and curvature partition across the eight-tick cycle each yield M/L = ϕ^n for integer n. The observed interval 100-550 matches ϕ^10 ≈ 123 to ϕ^13 ≈ 521. CycleLength is defined as the integer 8 counting events in one cycle. Upstream theorems supply ϕ > 1.6, ϕ^10 > 100, and ϕ^13 < 550.
proof idea
The term proof supplies the witness fun _ n => phi_power n for derive. Reflexivity confirms equality to phi_power. The existential is witnessed by n=10, with the lower bound taken directly from phi_10_bounds and the upper bound obtained by transitivity of ϕ^10 < ϕ^13 < 550 using zpow_lt_zpow_of_one_lt on phi_gt_one.
why it matters in Recognition Science
This theorem shows that the mass-to-light ratio is not an independent input but follows from the phi-ladder on the eight-tick cycle, closing the derivation gap stated in the module. It supports the framework claim that all dimensionless ratios are algebraic in phi, consistent with J-uniqueness and the self-similar fixed point. The result feeds cosmological predictions yet leaves the instability proof for non-phi-power values as an explicit scaffold.
scope and limits
- Does not derive the specific rung n from ledger topology.
- Does not prove instability of non-phi-power M/L values.
- Does not connect M/L directly to J-cost minimization.
- Does not address continuous or non-integer variations in M/L.
formal statement (Lean)
221theorem ml_is_derived_not_input :
222 ∃ (derive : ℕ → ℤ → ℝ),
223 (derive cycleLength = phi_power) ∧
224 (∃ n : ℤ, derive cycleLength n > 100 ∧ derive cycleLength n < 550) := by
proof body
Term-mode proof.
225 use fun _ n => phi_power n
226 constructor
227 · rfl
228 · use 10
229 constructor
230 · exact phi_10_bounds
231 · exact lt_trans (by
232 unfold phi_power
233 apply zpow_lt_zpow_of_one_lt phi_gt_one (by norm_num)
234 ) phi_13_bounds
235
236/-- **HYPOTHESIS**: Discrete uncertainty in M/L derivation.
237
238 STATUS: SCAFFOLD — The prediction that M/L uncertainty is discrete (following
239 the φ-ladder) follows from the J-cost topology, but the formal proof
240 that all intermediate values are unstable is a scaffold.
241
242 TODO: Formally prove the instability of non-φ-power M/L values. -/