rsConeModel_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove positivity for models other than the RS cone instantiation.
- Does not derive the constant values from any deeper Recognition Science equation.
- Does not address numerical evaluation beyond the exact integers supplied.
- Does not extend the result to variable or parameterized constants.
Lean usage
example : rsConeModel.energyGap () ≥ cmin rsConeModel.C * rsConeModel.defectMass () := Model.energyGap_ge_cmin_mul_defect rsConeModel rsConeModel_pos ()formal statement (Lean)
118lemma rsConeModel_pos :
119 0 < rsConeModel.C.Knet ∧ 0 < rsConeModel.C.Cproj ∧ 0 < rsConeModel.C.Ceng := by
proof body
Term-mode proof.
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. -/