def
definition
def or abbrev
ilgModel
show as:
view Lean formalization →
formal statement (Lean)
120noncomputable def ilgModel (P : KernelParams)
121 (h_energy : EnergyControlHypothesis P) : Model ILGState := {
proof body
Definition body.
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
151 simp only [hCeng, one_mul]
152 exact h_energy s,
153 dispersion := by
154 intro s
155 -- orthoMass ≤ C_disp * tests
156 -- Since tests = defectMass = orthoMass and C_disp = 1, this is equality
157 simp only [orthoMass, tests]
158 have h : ilgConstants.Cdisp = 1 := rfl
159 simp [h]
160}
161
162/-! ## Optional variational hypothesis (not used in the CPM instance above)
163
164Some downstream discussions of ILG use a Lax–Milgram style statement that a suitable
165projection decreases defect. We record it as a hypothesis (not an axiom) so callers
166can assume it explicitly when needed.
167
168Note: This definition is commented out because `ilgDefect` and `projOp` are not yet defined.
169When those are implemented, uncomment this hypothesis.
170
171-- def projection_decreases_defect_hypothesis (P : KernelParams) : Prop :=
172-- ∀ s : ILGState, ilgDefect P (projOp P s) ≤ ilgDefect P s
173-/
174
175/-! ## Coercivity Results -/
176
177/-- The ILG coercivity constant is 49/162. -/