pith. machine review for the scientific record. sign in
theorem proved term proof

ml_derivation_complete

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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
 181  · -- On φ-ladder
 182    use 1
 183    constructor
 184    · simp [Set.mem_insert_iff]
 185    · rw [zpow_one]; exact ml_derived_value
 186
 187/-! ## Zero-Parameter Status Certificate -/
 188
 189/-- **HYPOTHESIS**: All fundamental constants are derived from MP.
 190
 191    STATUS: SCAFFOLD — Needs unified mapping of all constant derivations.
 192    TODO: Create master certificate importing all constant derivation modules. -/

depends on (24)

Lean names referenced from this declaration's body.