EnergyControlHypothesis

formal source

 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
 138      apply mul_nonneg
 139      · apply sq_nonneg
 140      · exact s.baryonicMass_nonneg
 141    calc defectMass P s
 142        = 1 * defectMass P s := by ring
 143      _ ≤ (ilgConstants.Knet * ilgConstants.Cproj) * defectMass P s := by
 144          apply mul_le_mul_of_nonneg_right h hdef_nonneg,
 145  energy_control := by