coneConstants
plain-language theorem explainer
The declaration supplies the canonical RS-native constants for the cone projection in the Coercive Projection Method by setting Knet to 1, Cproj to 2, Ceng to 1 and Cdisp to 1. Researchers working on abstract coercivity models in CPM cite this instantiation to populate the generic Constants structure for downstream calculations such as cmin. The definition constructs the record directly and discharges the four non-negativity obligations via norm_num.
Claim. The RS-native cone projection constants are the tuple with $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$, each satisfying the non-negativity conditions $0≤K_{net}$, $0≤C_{proj}$, $0≤C_{eng}$, $0≤C_{disp}$.
background
The Constants structure is the abstract bundle of four real-valued CPM parameters (Knet, Cproj, Ceng, Cdisp) together with proofs of their non-negativity. This module supplies a domain-agnostic formalization of the Coercive Projection Method in three parts: projection-defect inequality, coercivity factorization in which the energy gap controls defect mass, and aggregation of local tests into membership. The upstream Constants definition supplies the record type that coneConstants populates with the RS-specific numerical values.
proof idea
The definition directly constructs the Constants record by assigning the four numerical fields and applies norm_num to each of the four non-negativity proofs.
why it matters
This supplies the concrete constants that downstream results such as cone_cmin_consistent and rs_cone_cmin_value rely on to obtain cmin = 1/2, and that rsConeModel and rsConeModel_pos instantiate for explicit coercivity checks. It anchors the RS cone model inside the abstract CPM A/B/C logic and supplies the values used by the J-cost normalization hook in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.