  94/-! ## Example 3: RS Cone Constants Model -/
  95
  96/-- Model using the canonical RS cone constants. -/
  97def rsConeModel : Model Unit := {
  98  C := RS.coneConstants,
  99  defectMass := fun _ => 1,
 100  orthoMass := fun _ => 1,
 101  energyGap := fun _ => 2,
 102  tests := fun _ => 1,
 103  projection_defect := by
 104    intro _
 105    simp only [RS.cone_Knet_eq_one, RS.cone_Cproj_eq_two]
 106    norm_num,
 107  energy_control := by
 108    intro _
 109    simp only [RS.cone_Ceng_eq_one]
 110    norm_num,
 111  dispersion := by
 112    intro _
 113    simp only [RS.cone_Cdisp_eq_one]
 114    norm_num
 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

papers checked against this theorem

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