NeutProtonDiff5Cert
plain-language theorem explainer
Certificate structure packing three structural properties used for the RS5 neutron-proton mass-difference argument: diagonal domain cost vanishes, domain cost is nonnegative on positive mass/energy, and the canonical threshold is positive. Downstream code inhabits it once and cites Nonempty. Pure definitional packaging; the three fields are discharged by sibling lemmas, not proved here.
Claim. A certificate for the RS5 neutron-proton difference is a triple of properties: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive mass and energy parameters $m,e>0$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
The module targets the neutron-proton mass gap $m_n-m_p=1.293,\mathrm{MeV}$ in Recognition Science units. The claimed RS identity is $J(\varphi)\cdot 10.96,\mathrm{MeV}=1.293,\mathrm{MeV}$ (equivalently $J(\varphi)$ times a corrected $m_W/45$ factor), where $J$ is the unique nonnegative cost from the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$.
Domain cost is the local cost functional on mass/energy pairs used in this RS5 session; the diagonal vanishing $C(r,r)=0$ encodes that equal arguments carry no defect. The canonical threshold is the positive cutoff against which the gap is compared. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states.
Status of the module is structural: zero sorry, zero axiom. The certificate is the Prop-bundle that later inhabitants must satisfy.
proof idea
No proof body: this is a structure declaration. The three fields are named hypotheses (diagonal vanishing of domain cost, nonnegativity of domain cost on positive arguments, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the structural side-conditions of the RS5 neutron-proton difference derivation, so later theorems can assume or inhabit one object rather than three loose lemmas. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty, closing the structural layer of the module.
In the broader framework this sits under Foundation cost calculus: $J$-uniqueness (T5), $\varphi$ as self-similar fixed point (T6), and the nonnegative $J$-cost that forces mass defects to sit above a positive floor. The numerical claim $m_n-m_p=1.293,\mathrm{MeV}$ is stated in the module doc as an exact $J(\varphi)$ scaling; this certificate does not itself compute that number, but packages the cost axioms any such computation must respect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.