theorem
proved
ml_in_observed_range
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Astrophysics.MassToLight on GitHub at line 150.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
all -
all -
ml_derived -
ml_derived_value -
phi_in_observed_range -
three_strategies_agree -
of -
all -
of -
of -
of -
of -
all -
and -
L -
M -
L -
M
used by
formal source
147
148/-- The derived M/L is in the observed range [0.5, 5] solar units.
149 Proof depends on the axiom ml_derived_value : ml_derived = φ. -/
150theorem ml_in_observed_range : 0.5 < ml_derived ∧ ml_derived < 5 := by
151 rw [ml_derived_value]
152 exact phi_in_observed_range
153
154/-! ## The Complete Derivation Certificate -/
155
156/-- **THEOREM (RIGOROUS given axioms)**: Complete M/L Derivation Certificate.
157
158 This theorem assembles all the components of the M/L derivation.
159 It depends on the physical axioms `ml_derived_value` and `three_strategies_agree`. -/
160theorem ml_derivation_complete :
161 -- The derived value
162 (ml_derived = φ) ∧
163 -- Three strategies agree
164 (StellarAssembly.ml_stellar = ml_derived) ∧
165 (NucleosynthesisTiers.ml_nucleosynthesis = ml_derived) ∧
166 (ObservabilityLimits.ml_geometric = ml_derived) ∧
167 -- In observed range
168 (0.5 < ml_derived ∧ ml_derived < 5) ∧
169 -- Quantized on φ-ladder (n = 1 gives φ^1 = φ)
170 (∃ n : ℤ, n ∈ ({0, 1, 2, 3} : Set ℤ) ∧ ml_derived = φ ^ n) := by
171 have h_agree := three_strategies_agree
172 refine ⟨ml_derived_value, ?_, ?_, ?_, ml_in_observed_range, ?_⟩
173 · -- StellarAssembly agrees
174 have ⟨h1, h2, h3⟩ := h_agree
175 rw [h1, h2, h3]
176 · -- NucleosynthesisTiers agrees
177 have ⟨_, h2, h3⟩ := h_agree
178 rw [h2, h3]
179 · -- ObservabilityLimits agrees
180 exact h_agree.2.2