phi_bounds

formal source

 130    linarith
 131
 132/-- **THEOREM (RIGOROUS)**: φ is strictly between 1 and 2. -/
 133theorem phi_bounds : 1 < φ ∧ φ < 2 := by
 134  constructor
 135  · -- 1 < φ: Since √5 > 1, we have (1 + √5)/2 > 1
 136    unfold φ Constants.phi
 137    have h_sqrt5_gt_1 : 1 < Real.sqrt 5 := by
 138      rw [show (1 : ℝ) = Real.sqrt 1 by norm_num]
 139      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
 140    linarith
 141  · -- φ < 2: Since √5 < 3, we have (1 + √5)/2 < 2
 142    unfold φ Constants.phi
 143    have h_sqrt5_lt_3 : Real.sqrt 5 < 3 := by
 144      rw [show (3 : ℝ) = Real.sqrt 9 by norm_num]
 145      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
 146    linarith
 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