rs_cone_cmin_value
plain-language theorem explainer
The lemma establishes that the coercivity constant c_min for the RS cone constants equals one half. Researchers instantiating CPM models with RS-native values cite this to anchor the baseline coercivity for cone projections. The proof is a direct term-mode simplification that substitutes the explicit cone constant values and evaluates the resulting reciprocal.
Claim. The coercivity constant satisfies $c_ {min} = 1/2$ for the RS cone constants, where $c_{min} = 1/(K_{net} · C_{proj} · C_{eng})$ with the values $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$.
background
In the CPM framework the coercivity constant is defined by $c_{min}(C) = (K_{net} · C_{proj} · C_{eng})^{-1}$ for any Constants record C. The RS cone model supplies the concrete record coneConstants with K_net = 1, C_proj = 2, C_eng = 1 (and C_disp = 1), together with the equality lemmas that expose these values directly.
proof idea
The term proof applies simp with the lemmas cmin, cone_Knet_eq_one, cone_Cproj_eq_two and cone_Ceng_eq_one to reduce the expression to the reciprocal of 2, then closes with norm_num.
why it matters
This result validates the RS cone model inside the CPM examples module and confirms the coercivity value that accompanies the eight-tick octave constants. It supports downstream testing of the core CPM theorems without deriving the constants from the forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.