`eightTickModel_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.CPM.Examples
domain: CPM
line: 165 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CPM.Examples on GitHub at line 165.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 162  norm_num
 163
 164/-- Verify positivity of eight-tick constants. -/
 165lemma eightTickModel_pos :
 166    0 < eightTickModel.C.Knet ∧ 0 < eightTickModel.C.Cproj ∧ 0 < eightTickModel.C.Ceng := by
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.