rs_cone_cmin_value

formal source

 124  Model.energyGap_ge_cmin_mul_defect rsConeModel rsConeModel_pos ()
 125
 126/-- The RS cone coercivity constant is 1/2. -/
 127lemma rs_cone_cmin_value : cmin RS.coneConstants = 1 / 2 := by
 128  simp only [cmin, RS.cone_Knet_eq_one, RS.cone_Cproj_eq_two, RS.cone_Ceng_eq_one]
 129  norm_num
 130
 131/-! ## Example 4: Eight-Tick Net Constants Model -/
 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}