ml_derivation_falsifiable
plain-language theorem explainer
The theorem asserts that any observed mass-to-light ratio lying outside the closed interval [0.5, 5] solar units cannot equal the derived value, while that derived value equals the golden ratio φ. Astrophysicists checking Recognition Science predictions against stellar data would cite the result to establish falsifiability of the zero-parameter framework. The proof splits the conjunction via constructor, derives a contradiction in the first conjunct from the interval membership of the derived value, and invokes the direct equality in the second
Claim. Let $m$ denote the derived stellar mass-to-light ratio. Then for every real number $o$, if $o$ lies outside the interval $[0.5,5]$ it follows that $o$ differs from $m$, and moreover $m$ equals the golden ratio $φ$.
background
The module derives the stellar mass-to-light ratio from Recognition Science by three independent routes. Strategy 1 weights photon emission against mass storage by the J-cost function, yielding $M/L = φ^n$. Strategy 2 places nuclear densities and photon fluxes on discrete φ-tiers so that $M/L = φ^{Δn}$. Strategy 3 combines geometric observability limits with J-minimization to force the same ladder values. All three converge on the single characteristic value $m = φ ≈ 1.618$ solar units, with the admissible set {1, φ, φ², φ³} lying inside the observed window [0.5, 5]. Upstream, ml_derived is defined as Constants.phi and ml_derived_value records the trivial equality $m = φ$. The companion theorem ml_in_observed_range then asserts $0.5 < m ∧ m < 5$ by rewriting with that equality and applying the phi bounds lemma.
proof idea
The term-mode proof opens with constructor to separate the two conjuncts. For the first conjunct the tactic intro assumes an observation obs outside [0.5,5] together with the equality obs = ml_derived; rewriting the equality into the membership hypothesis produces a contradiction once the interval bounds from ml_in_observed_range are unpacked and applied. The second conjunct is discharged by the one-line exact application of ml_derived_value.
why it matters
The declaration closes the derivation certificate for the mass-to-light ratio, thereby completing the module claim that Recognition Science reaches true zero-parameter status once all astrophysical calibrations are obtained from the ledger structure. It sits downstream of the three-strategy agreement hypothesis and the phi-ladder construction, and directly supports the summary table asserting zero adjustable parameters. Within the broader framework the result instantiates the T5 J-uniqueness and T6 phi fixed-point steps by showing that the same self-similar constant governs stellar observables, furnishing an explicit falsification criterion for the entire T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.