Pith. sign in
module module low

IndisputableMonolith.Foundation.Neutron_Proton_Diff_RS5

show as:
view Lean formalization →

Module packaging an RS certificate for the neutron–proton mass difference under a domain cost and a positive canonical threshold. Particle-physics and RS-mass auditors cite it when checking that the n–p gap sits inside the allowed cost band. Structure is definitional: cost and threshold, nonnegativity and positivity lemmas, then an inhabited certificate record.

claimDefines a domain cost $C$, proves $C \ge 0$ and evaluates it at equality cases, fixes a canonical threshold $\theta > 0$, and packages an inhabited certificate $\mathrm{NeutProtonDiff5Cert}$ asserting that the neutron–proton mass difference meets the RS cost/threshold constraints.

background

Recognition Science places hadron masses on a $\varphi$-ladder (yardstick times $\varphi$ to a rung offset by a charge-dependent gap). The neutron–proton splitting is then a small rung/gap discrepancy rather than an independent parameter. Cost is the standard RS $J$-cost infrastructure imported from Cost, with constants (including the tick $\tau_0$) from Constants.

This module stays inside Foundation: it does not re-derive the ladder, but introduces a domain-restricted cost, a canonical numerical threshold, and a certificate type whose inhabitation is the local claim that the $n$–$p$ difference is admissible under those bounds.

proof idea

Definition-and-certificate module, not a deep derivation. It introduces domainCost with equality and nonnegativity lemmas, defines canonicalThreshold with a positivity proof, then builds NeutProtonDiff5Cert and exhibits cert via cert_inhabited. Argument shape is: set cost and threshold, discharge the elementary inequalities, inhabit the certificate record.

why it matters in Recognition Science

Closes a Foundation-level certificate for the neutron–proton mass gap inside the RS mass story (phi-ladder with rung/gap structure). No downstream used_by edges are recorded yet, so the module is a leaf certificate rather than an input to a named parent theorem. It sits beside the broader RS mass and forcing chain (T5–T8, RCL, $\varphi$) as a concrete hadronic check: if the certificate fails, the claimed $n$–$p$ placement on the ladder is untenable under the stated cost bound.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)