ilgConstants

formal source

  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
 111/-- Energy control hypothesis: the energy of a configuration bounds its defect.
 112    This is the physical content of the variational principle (Lax-Milgram).
 113    In ILG, this states that the gravitational energy controls the deviation
 114    from the Newtonian solution. -/
 115def EnergyControlHypothesis (P : KernelParams) : Prop :=
 116  ∀ s : ILGState, defectMass P s ≤ energyGap s
 117
 118/-- The ILG model satisfies CPM assumptions when the energy control hypothesis holds.
 119    This makes the physical assumption explicit rather than hiding it in an unfinished proof. -/
 120noncomputable def ilgModel (P : KernelParams)
 121    (h_energy : EnergyControlHypothesis P) : Model ILGState := {
 122  C := ilgConstants,
 123  defectMass := defectMass P,
 124  orthoMass := orthoMass P,
 125  energyGap := energyGap,