rsConeModel_pos
plain-language theorem explainer
The lemma confirms that the RS cone model has strictly positive network stiffness, projection coefficient, and energy coefficient. Researchers applying the CPM coercivity bound would cite it to instantiate the canonical RS constants. The proof is a term-mode one-liner that refines the conjunction and normalizes the explicit constant values.
Claim. For the RS cone model with constants satisfying $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, the inequalities $0<K_{net}$, $0<C_{proj}$, and $0<C_{eng}$ hold.
background
The CPM framework defines a Model as a structure with constants C (containing K_net, C_proj, C_eng), a defect mass function, an orthogonal mass function, an energy gap function, and a tests function. The RS cone model is the instantiation that uses cone constants with the listed positive values together with unit defect and orthogonal masses. This module supplies concrete models to exercise the abstract theorems, including the coercivity result that requires the three constants to be positive so that c_min (the reciprocal of their product) is well-defined and positive.
proof idea
The proof is a term-mode one-liner. It refines the three-way conjunction into separate goals and applies norm_num to the definitions of the RS cone model and its cone constants, which are set to the explicit positive numbers 1, 2, and 1.
why it matters
The lemma supplies the positivity hypothesis needed to invoke energyGap_ge_cmin_mul_defect on the RS cone model, as demonstrated by the immediate example that verifies the energy-gap lower bound. It therefore completes the validation pattern for the canonical RS constants inside the CPM examples module. No open questions or scaffolding are involved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.