ilgModel

formal source

 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
 146    intro s
 147    -- orthoMass ≤ C_eng * energyGap
 148    -- Since C_eng = 1 and orthoMass = defectMass, this is defectMass ≤ energyGap
 149    simp only [orthoMass, energyGap, defectMass]
 150    have hCeng : ilgConstants.Ceng = 1 := rfl