matchesRSCore
plain-language theorem explainer
A constants bundle matches the Recognition Science core when its network constant equals 1 and its cone-projection constant equals 2. Energy and dispersion constants stay unconstrained. Initiality and universality arguments cite this predicate to test whether multi-domain CPM data sit on the RS cone. It is a two-literal propositional definition, not a proved theorem.
Claim. For a CPM constants bundle $C=(K_{\mathrm{net}},C_{\mathrm{proj}},C_{\mathrm{eng}},C_{\mathrm{disp}})$, write $\mathrm{matchesRSCore}(C)$ for the proposition $K_{\mathrm{net}}=1\land C_{\mathrm{proj}}=2$. The energy and dispersion components are left free.
background
The CPM Law of Existence packages four real constants into a single bundle: a nonnegative network constant $K_{\mathrm{net}}$, a cone-projection constant $C_{\mathrm{proj}}$, plus energy and dispersion scales $C_{\mathrm{eng}}$ and $C_{\mathrm{disp}}$. Recognition Science fixes the first two at the cone values $(1,2)$ while treating the latter pair as domain-dependent.
This module is a lightweight initiality-style bridge from CPM to RS. It records constants across independent domains (Hodge, RH, Navier–Stokes, Goldbach) and asks when those bundles sit on the same $(K_{\mathrm{net}},C_{\mathrm{proj}})$ pair as the RS signature. Matching on those two invariants is the structural gate before any uniqueness or exclusivity claim.
Upstream, the Constants structure supplies the four fields and the nonnegativity side condition on $K_{\mathrm{net}}$. The present definition simply names the RS core slice of that structure.
proof idea
Definitional, not a proof. The predicate is the conjunction $C.K_{\mathrm{net}}=1\land C.C_{\mathrm{proj}}=2$ on a Constants bundle. No tactics, no lemmas: the body is the Prop itself. Downstream theorems unfold it with dsimp or rcases on the two equalities.
why it matters
This is the gate predicate for the CPM-to-RS initiality skeleton. The local theorem universality_implies_RS_core takes a four-domain universality package whose Hodge, RH, NS, and Goldbach bundles all satisfy the predicate and concludes that the RS signature itself satisfies it, so RS is a valid universal witness. The companion universality_constants_agree extracts numerical agreement of $(K_{\mathrm{net}},C_{\mathrm{proj}})$ with the RS signature from the same hypothesis.
Both results are re-exported from CPMBridge.Exports, so verification clients cite this name rather than the internal module path. In the broader framework it records the cone-projection invariants that the forcing chain and exclusivity arguments treat as RS-native; it does not yet deliver the full category-theoretic uniqueness proof the module doc flags as future work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.