three_strategies_agree

formal source

  98
  99/-- **THEOREM (PROVED): Consistency of M/L Strategies**
 100    The thermodynamic, scaling, and architectural derivations agree. -/
 101theorem three_strategies_agree : H_ThreeStrategiesAgree := by
 102  unfold H_ThreeStrategiesAgree
 103  refine ⟨?_, ?_, ?_⟩
 104  · -- StellarAssembly = NucleosynthesisTiers
 105    -- Both are Constants.phi
 106    rw [StellarAssembly.ml_stellar_value, NucleosynthesisTiers.ml_nucleosynthesis_eq_phi]
 107    simp only [StellarAssembly.φ, NucleosynthesisTiers.φ]
 108  · -- NucleosynthesisTiers = ObservabilityLimits
 109    rw [NucleosynthesisTiers.ml_nucleosynthesis_eq_phi, ObservabilityLimits.ml_geometric_is_phi]
 110    simp only [NucleosynthesisTiers.φ, ObservabilityLimits.φ]
 111  · -- ObservabilityLimits = ml_derived
 112    rw [ObservabilityLimits.ml_geometric_is_phi, ml_derived_value]
 113    simp only [ObservabilityLimits.φ, φ]
 114
 115/-- **THEOREM (RIGOROUS)**: φ is in the observed range [0.5, 5] solar units.
 116
 117    This proves the range property for the φ value itself. Once `ml_derived_value`
 118    is proven (showing ml_derived = φ), this immediately gives `ml_in_observed_range`. -/
 119theorem phi_in_observed_range : 0.5 < φ ∧ φ < 5 := by
 120  constructor
 121  · -- 0.5 < φ: Since φ = (1 + √5)/2 and √5 > 0, we have φ > 0.5
 122    unfold φ Constants.phi
 123    have h_sqrt5_pos : 0 < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num : (5 : ℝ) > 0)
 124    linarith
 125  · -- φ < 5: Since φ = (1 + √5)/2 and √5 < 3, we have φ < 2 < 5
 126    unfold φ Constants.phi
 127    have h_sqrt5_lt_3 : Real.sqrt 5 < 3 := by
 128      rw [show (3 : ℝ) = Real.sqrt 9 by norm_num]
 129      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
 130    linarith
 131