pith. machine review for the scientific record. sign in
lemma proved tactic proof

eightTickModel_pos

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 165lemma eightTickModel_pos :
 166    0 < eightTickModel.C.Knet ∧ 0 < eightTickModel.C.Cproj ∧ 0 < eightTickModel.C.Ceng := by

proof body

Tactic-mode proof.

 167  simp only [eightTickModel]
 168  norm_num
 169
 170/-- Verify coercivity applies to eight-tick model. -/
 171example : eightTickModel.energyGap () ≥ cmin eightTickModel.C * eightTickModel.defectMass () :=
 172  Model.energyGap_ge_cmin_mul_defect eightTickModel eightTickModel_pos ()
 173
 174/-! ## Demonstration: cpmsimp tactic -/
 175
 176/-- Demonstration that `cpmsimp` normalizes products correctly. -/
 177example (a b c d : ℝ) : a * b * c * d = a * (b * c) * d := by cpmsimp
 178
 179example (a b c : ℝ) : a * b * c = b * a * c := by cpmsimp
 180
 181end Examples
 182end CPM
 183end IndisputableMonolith

depends on (10)

Lean names referenced from this declaration's body.