rsConeModel_pos
plain-language theorem explainer
The lemma establishes that the RS cone model has strictly positive K_net, C_proj and C_eng. Researchers applying coercivity bounds in CPM would cite it to invoke the energy-gap inequality. The proof is a one-line wrapper that applies norm_num to the explicit constants supplied by rsConeModel and coneConstants.
Claim. $0 < K_{net} ∧ 0 < C_{proj} ∧ 0 < C_{eng}$ where these are the three constants of the RS cone model (K_net = 1, C_proj = 2, C_eng = 1).
background
The CPM module supplies an abstract Model structure whose fields are a Constants record (K_net, C_proj, C_eng, …) together with defectMass, orthoMass, energyGap and tests maps. The RS cone model is the concrete instantiation that sets defectMass = orthoMass = 1, energyGap = 2 and C := coneConstants. coneConstants itself is the record with K_net = 1, C_proj = 2, C_eng = 1 (and non-negativity proofs). cmin is defined as the reciprocal of the product K_net · C_proj · C_eng; the positivity lemma cmin_pos therefore requires exactly the three strict inequalities proved here.
proof idea
one-line wrapper that applies norm_num to unfold rsConeModel and coneConstants, discharging the three conjuncts by direct arithmetic on the literal values 1, 2 and 1.
why it matters
The lemma is the positivity hypothesis required by energyGap_ge_cmin_mul_defect, which is then exercised in the immediately following example. It therefore closes the verification loop for the canonical RS constants inside the CPM example suite. The constants themselves are the concrete link between the abstract CPM coercivity statement and the Recognition Science cone-projection values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.