lemma proved term proof

`rs_cone_cmin_value`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 127lemma rs_cone_cmin_value : cmin RS.coneConstants = 1 / 2 := by

proof body

Term-mode proof.

 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. -/

depends on (15)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
cmin in IndisputableMonolith.CPM.LawOfExistence decl_use
cone_Ceng_eq_one in IndisputableMonolith.CPM.LawOfExistence decl_use
coneConstants in IndisputableMonolith.CPM.LawOfExistence decl_use
cone_Cproj_eq_two in IndisputableMonolith.CPM.LawOfExistence decl_use
cone_Knet_eq_one in IndisputableMonolith.CPM.LawOfExistence decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
Model in IndisputableMonolith.CPM.LawOfExistence decl_use
Tick in IndisputableMonolith.Foundation.TimeEmergence decl_use
C_proj in IndisputableMonolith.Gravity.CoerciveProjection decl_use
K_net in IndisputableMonolith.Gravity.CoerciveProjection decl_use
Tick in IndisputableMonolith.Masses.Ribbons decl_use
Tick in IndisputableMonolith.Masses.Ribbons.Tick decl_use
Tick in IndisputableMonolith.Measurement.RSNative.Core decl_use