rsConeModel_pos

formal source

 115}
 116
 117/-- Verify the RS model has positive constants. -/
 118lemma rsConeModel_pos :
 119    0 < rsConeModel.C.Knet ∧ 0 < rsConeModel.C.Cproj ∧ 0 < rsConeModel.C.Ceng := by
 120  refine ⟨?_, ?_, ?_⟩ <;> norm_num [rsConeModel, RS.coneConstants]
 121
 122/-- Verify coercivity with explicit c_min for RS model. -/
 123example : rsConeModel.energyGap () ≥ cmin rsConeModel.C * rsConeModel.defectMass () :=
 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,