`ilg_coercivity`

proved

show as: view math explainer →

module: IndisputableMonolith.ILG.CPMInstance
domain: ILG
line: 188 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ILG.CPMInstance on GitHub at line 188.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.