ilg_reverse_coercivity

formal source

 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
 209/-! ## Falsifiability Bounds -/
 210
 211/-- Structure recording falsifiable predictions for ILG. -/
 212structure ILGPrediction where
 213  /-- Predicted rotation curve enhancement factor -/
 214  enhancement : ℝ
 215  /-- Uncertainty bound -/
 216  uncertainty : ℝ
 217  /-- The enhancement is bounded by the kernel -/
 218  enhancement_bounded : enhancement ≤ 2
 219
 220/-- The ILG kernel provides a falsifiable upper bound on dark matter effects. -/
 221theorem ilg_falsifiable_bound (P : KernelParams) (k a : ℝ) :
 222    kernel P k a ≥ 1 := kernel_ge_one P k a
 223
 224end ILG
 225end IndisputableMonolith