ilgConeConstants

formal source

 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,
 126  tests := tests P,
 127  projection_defect := by
 128    intro s
 129    -- D ≤ K_net · C_proj · O
 130    -- Since orthoMass = defectMass for ILG, we need K_net · C_proj ≥ 1
 131    simp only [defectMass, orthoMass]
 132    have h : ilgConstants.Knet * ilgConstants.Cproj ≥ 1 := by
 133      simp [ilgConstants]
 134      norm_num
 135    -- defectMass ≤ K_net * C_proj * defectMass when K_net * C_proj ≥ 1
 136    have hdef_nonneg : 0 ≤ defectMass P s := by
 137      unfold defectMass