def
definition
def or abbrev
eightTickModel
show as:
view Lean formalization →
formal statement (Lean)
135noncomputable def eightTickModel : Model Unit := {
proof body
Definition body.
136 C := {
137 Knet := (9/7)^2,
138 Cproj := 2,
139 Ceng := 1,
140 Cdisp := 1,
141 Knet_nonneg := by norm_num,
142 Cproj_nonneg := by norm_num,
143 Ceng_nonneg := by norm_num,
144 Cdisp_nonneg := by norm_num
145 },
146 defectMass := fun _ => 1,
147 orthoMass := fun _ => 1,
148 energyGap := fun _ => 4,
149 tests := fun _ => 1,
150 projection_defect := by
151 intro _
152 -- Need: 1 ≤ (9/7)^2 * 2 * 1
153 have h : (1 : ℝ) ≤ (9/7)^2 * 2 := by norm_num
154 linarith,
155 energy_control := by intro _; norm_num,
156 dispersion := by intro _; norm_num
157}
158
159/-- The eight-tick coercivity constant is 49/162. -/