theorem
proved
rs_zero_parameter_status
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Astrophysics.MassToLight on GitHub at line 210.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
207
208/-- **THEOREM (PROVED): RS Zero-Parameter Status**
209 The RS derivation chain introduces zero adjustable parameters. -/
210theorem rs_zero_parameter_status : H_RSZeroParameterStatus := by
211 unfold H_RSZeroParameterStatus
212 constructor
213 · use (fun _ => Constants.phi)
214 exact ml_derived_value
215 · exact ⟨Constants.phi, rfl⟩
216
217/-- **THEOREM (RIGOROUS)**: The M/L derivation is falsifiable -/
218theorem ml_derivation_falsifiable :
219 -- If observed M/L differs significantly from φ-ladder, theory is falsified
220 (∀ obs : ℝ, obs ∉ Set.Icc 0.5 5 → obs ≠ ml_derived) ∧
221 -- Specific prediction
222 (ml_derived = φ) := by
223 constructor
224 · intro obs hobs h
225 -- If obs = ml_derived, then obs ∈ [0.5, 5] by ml_in_observed_range
226 rw [h] at hobs
227 have ⟨h1, h2⟩ := ml_in_observed_range
228 apply hobs
229 exact ⟨le_of_lt h1, le_of_lt h2⟩
230 · exact ml_derived_value
231
232/-! ## Summary -/
233
234/-- Summary of the M/L derivation:
235
236| Property | Value |
237|----------|-------|
238| Characteristic M/L | φ ≈ 1.618 solar units |
239| Valid range | {1, φ, φ², φ³} = {1, 1.618, 2.618, 4.236} |
240| Observed range | [0.5, 5] solar units ✓ |