ilg_cmin_value

formal source

 175/-! ## Coercivity Results -/
 176
 177/-- The ILG coercivity constant is 49/162. -/
 178theorem ilg_cmin_value : cmin ilgConstants = 49 / 162 := by
 179  simp [cmin, ilgConstants]
 180  norm_num
 181
 182/-- Positivity of ILG constants. -/
 183theorem ilgConstants_pos :
 184    0 < ilgConstants.Knet ∧ 0 < ilgConstants.Cproj ∧ 0 < ilgConstants.Ceng := by
 185  refine ⟨?_, ?_, ?_⟩ <;> simp only [ilgConstants] <;> norm_num
 186
 187/-- The coercivity theorem for ILG: energy gap controls defect mass. -/
 188theorem ilg_coercivity (P : KernelParams) (h_energy : EnergyControlHypothesis P) (s : ILGState) :
 189    (ilgModel P h_energy).defectMass s ≤
 190    ((ilgModel P h_energy).C.Knet * (ilgModel P h_energy).C.Cproj * (ilgModel P h_energy).C.Ceng) *
 191    (ilgModel P h_energy).energyGap s :=
 192  (ilgModel P h_energy).defect_le_constants_mul_energyGap s
 193
 194/-- Reverse coercivity: energy gap is at least c_min times defect. -/
 195theorem ilg_reverse_coercivity (P : KernelParams) (h_energy : EnergyControlHypothesis P) (s : ILGState) :
 196    (ilgModel P h_energy).energyGap s ≥ cmin (ilgModel P h_energy).C * (ilgModel P h_energy).defectMass s :=
 197  (ilgModel P h_energy).energyGap_ge_cmin_mul_defect ilgConstants_pos s
 198
 199/-! ## Connection to RS Constants -/
 200
 201/-- The ILG exponent α matches the RS-canonical value. -/
 202theorem ilg_alpha_eq_rs (tau0 : ℝ) (h : 0 < tau0) :
 203    (rsKernelParams tau0 h).alpha = alphaLock := rfl
 204
 205/-- The eight-tick coercivity constant 49/162 matches the CPM prediction. -/
 206theorem ilg_c_matches_cpm : (49 : ℝ) / 162 = cmin ilgConstants := by
 207  rw [ilg_cmin_value]
 208