`eightTickModel`

definition

show as: view math explainer →

module: IndisputableMonolith.CPM.Examples
domain: CPM
line: 135 · 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 135.

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

used by

formal source

 132
 133/-- Model using the eight-tick aligned constants (K_net = (9/7)², C_proj = 2).
 134This matches the constants derived in the LaTeX support document. -/
 135noncomputable def eightTickModel : Model Unit := {
 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. -/
 160lemma eight_tick_cmin_value : cmin eightTickModel.C = 49 / 162 := by
 161  simp only [cmin, eightTickModel]
 162  norm_num
 163
 164/-- Verify positivity of eight-tick constants. -/
 165lemma eightTickModel_pos :

papers checked against this theorem

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