universality_constants_agree
plain-language theorem explainer
Under a four-domain universality hypothesis (Hodge, RH, Navier–Stokes, Goldbach), if each domain’s CPM constants match the RS core invariants, then the Hodge constants agree with the RS witness on the pair $(K_{\mathrm{net}},C_{\mathrm{proj}})$. Cited by anyone wiring CPM domain signatures into the RS initiality bridge. Proof is a short case-split: unpack the Hodge match and rewrite against the two cone-constant simp lemmas.
Claim. Let $U$ be a universality package of four domain signatures (Hodge, RH, Navier–Stokes, Goldbach). If each domain’s constants match the RS core on the cone invariants ($K_{\mathrm{net}}=1$ and $C_{\mathrm{proj}}=2$), then the Hodge constants equal the RS signature constants on those same two components: $K_{\mathrm{net}}^{\mathrm{Hodge}}=K_{\mathrm{net}}^{\mathrm{RS}}$ and $C_{\mathrm{proj}}^{\mathrm{Hodge}}=C_{\mathrm{proj}}^{\mathrm{RS}}$.
background
This module is a lightweight CPM-to-RS initiality skeleton. It records CPM constants for several independent mathematical domains and shows that matching the RS cone-projection invariants forces a unique constants witness coinciding with the RS instance, preparing a later category-theoretic uniqueness argument and physics-side exclusivity.
A Universality package is four FrameworkSig records (Hodge, RH, NS, Goldbach). The RS witness RS_sig is the framework signature built from RS.coneConstants. Matching the RS core means the two key invariants agree: net connectivity $K_{\mathrm{net}}=1$ and cone projection $C_{\mathrm{proj}}=2$; energy and dispersion constants stay free.
Upstream, those two equalities are definitional simp facts on the cone constants bundle: cone_Knet_eq_one and cone_Cproj_eq_two.
proof idea
Tactic proof, not a wrapper. Destructure the four-way match hypothesis and keep only the Hodge conjunct; unpack that into the two core equalities $K_{\mathrm{net}}=1$ and $C_{\mathrm{proj}}=2$. Split the goal conjunction. For each side, unfold the RS signature definition, rewrite by the corresponding Hodge equality, and finish with the cone simp lemma (cone_Knet_eq_one or cone_Cproj_eq_two). The RH, NS, and Goldbach match hypotheses are unused in this statement.
why it matters
Inside the CPM⇒RS bridge, this is the constants-level agreement step: once universality supplies core matches across domains, the RS cone pair $(K_{\mathrm{net}},C_{\mathrm{proj}})=(1,2)$ is recovered on the Hodge slot of the package, so the RS signature is the universal constants witness at those invariants.
The module doc frames this as stage-setting for a full initiality/uniqueness proof and for integration with exclusivity on the physics side. No downstream consumers are wired yet (used_by is empty), so the lemma is presently a leaf in the verification graph rather than a cited stepping stone.
It does not itself invoke the forcing chain T0–T8, the Recognition Composition Law, or the mass ladder; it only locks the two cone invariants that the Law of Existence package exposes as the RS core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.