rsConeModel
plain-language theorem explainer
rsConeModel instantiates the abstract CPM Model over the unit state space using the canonical RS cone constants with K_net = 1, C_proj = 2, C_eng = 1, C_disp = 1. Researchers validating CPM infrastructure or testing coercivity conditions would cite this example. The definition constructs the record directly from coneConstants and constant functions, discharging the required field proofs via simp and norm_num on the cone equality lemmas.
Claim. The RS cone model is the CPM model $M : Model(Unit)$ with constants $C = coneConstants$ where $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$, defect mass and orthogonal mass constantly equal to 1, energy gap constantly 2, tests constantly 1, and the projection defect, energy control, and dispersion conditions holding by direct evaluation.
background
The CPM framework defines an abstract Model structure consisting of a Constants bundle (K_net, C_proj, C_eng, C_disp with nonnegativity) together with functions for defectMass, orthoMass, energyGap, tests on the state space, plus proof obligations for projection_defect, energy_control, and dispersion. In this module, examples instantiate this structure to test core theorems from LawOfExistence. The coneConstants definition supplies the RS-native values K_net := 1, C_proj := 2, C_eng := 1, C_disp := 1, justified by the J-cost normalization lemmas cone_Knet_eq_one, cone_Cproj_eq_two, cone_Ceng_eq_one, cone_Cdisp_eq_one which state these equalities by reflexivity.
proof idea
The definition is a direct record literal. It sets C to coneConstants, assigns constant functions for the mass and gap fields, and discharges the three proof fields by applying simp only on the corresponding cone equality lemmas followed by norm_num.
why it matters
This definition supplies the canonical RS cone model that is used by rsConeModel_pos to verify positive constants and coercivity. It fills the role of testing the canonical RS constants in the CPM examples, as described in the module documentation. It connects to the LawOfExistence theorems that establish the cone constants via the J-cost log-coordinate normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.