energyGap

formal source

  77
  78/-- Energy gap: excess energy above the Newtonian ground state.
  79    Proportional to the integral of (∇w)² + potential terms. -/
  80noncomputable def energyGap (s : ILGState) : ℝ :=
  81  s.energy
  82
  83/-- Test functional: supremum over local tests (for aggregation theorem).
  84    In the gravitational context, this represents local curvature bounds. -/
  85noncomputable def tests (P : KernelParams) (s : ILGState) : ℝ :=
  86  defectMass P s
  87
  88/-! ## CPM Constants for ILG -/
  89
  90/-- ILG-specific CPM constants derived from eight-tick geometry.
  91    - K_net = (9/7)² from ε = 1/8 covering
  92    - C_proj = 2 from J''(1) = 1 normalization
  93    - C_eng = 1 standard energy normalization
  94    - C_disp = 1 dispersion bound -/
  95noncomputable def ilgConstants : Constants := {
  96  Knet := (9/7)^2,
  97  Cproj := 2,
  98  Ceng := 1,
  99  Cdisp := 1,
 100  Knet_nonneg := by norm_num,
 101  Cproj_nonneg := by norm_num,
 102  Ceng_nonneg := by norm_num,
 103  Cdisp_nonneg := by norm_num
 104}
 105
 106/-- Alternative: RS cone constants (K_net = 1). -/
 107def ilgConeConstants : Constants := RS.coneConstants
 108
 109/-! ## CPM Model Instantiation -/
 110