cert
plain-language theorem explainer
Packages three elementary facts about the neutron–proton domain cost into a single certificate: the cost vanishes on the diagonal, stays non-negative for positive mass and energy arguments, and the canonical threshold is strictly positive. Anyone citing the RS5 neutron–proton mass-difference module uses this bundle as the standing hypothesis package. The definition is a pure structure instance that wires three already-proved sibling lemmas.
Claim. There exists a certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the neutron–proton mass split in Recognition Science units. The experimental anchor is $m_n-m_p=1.293,\mathrm{MeV}$, recovered in RS as $J(\varphi)\cdot 10.96,\mathrm{MeV}$ (equivalently $J(\varphi)$ times a corrected $m_W/45$ factor). Here $J$ is the unique cost functional forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$.
Domain cost is the local cost functional on pairs of positive reals that the module uses to compare neutron and proton mass scales. The canonical threshold is the positive cutoff against which that cost is judged. The certificate structure simply records the three algebraic properties any such cost must satisfy before the mass-difference identity is invoked.
Upstream, non-negativity of recognition cost is already known from ObserverForcing: every recognition event has $J$-cost at least zero, with the identity event sitting at the global minimum $x=1$.
proof idea
One-line structure instance. The three fields of NeutProtonDiff5Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No additional tactic work occurs; the definition is pure packaging.
why it matters
The module is marked STRUCTURAL THEOREM (zero sorry, zero axiom) and claims an exact RS derivation of the $1.293,\mathrm{MeV}$ neutron–proton split via $J(\varphi)$. This certificate is the local hypothesis bundle that any later numerical or ladder identity in the same file can assume without re-proving the three elementary cost facts. It sits downstream of the global $J$-cost non-negativity theorem and upstream of any concrete comparison of neutron versus proton rungs on the $\varphi$-ladder. No further parent theorems currently depend on it (used-by is empty), so its role is modular hygiene inside the RS5 mass-difference session.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.