cone_Cdisp_eq_one
plain-language theorem explainer
The lemma fixes the dispersion coefficient at unity inside the canonical RS cone projection constants. Modelers instantiating the abstract Coercive Projection Method for Recognition Science examples cite this normalization to close the constant set. The proof is a direct reflexivity step that matches the literal assignment in the defining record.
Claim. In the RS-native constants for cone projection, the dispersion coefficient satisfies $C_{disp}=1$.
background
The module supplies an abstract, domain-agnostic formalization of the Coercive Projection Method with three layers: projection-defect inequality, coercivity factorization via energy gap, and aggregation from local tests. coneConstants records the RS-native values Knet=1, Cproj=2, Ceng=1, Cdisp=1. The cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the underlying J-cost, while the ContinuumBridge structure identifies the discrete Laplacian action with the simplicial defect sum.
proof idea
The proof is a one-line term-mode reflexivity that matches the literal value assigned to Cdisp inside the coneConstants record.
why it matters
The normalization is consumed by rsConeModel, which builds the concrete Model instance used in CPM examples. It supplies the required unit value for the dispersion term in the abstract CPM framework, consistent with the Recognition Science convention of normalized coefficients in the cone projection step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.