RSPhysics003Cert
plain-language theorem explainer
Certificate bundle for RS Physics Module 3 (neutron lifetime). It requires three structural facts: domain cost vanishes on equal arguments, domain cost is nonnegative for positive mass and energy, and the canonical threshold is positive. Downstream code supplies a concrete inhabitant and proves the type is nonempty. Pure structure definition; no proof body.
Claim. A certificate for the neutron-lifetime physics module is a triple of properties: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all reals $m>0$ and $e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 3 records the RS neutron-lifetime claim $\phi^{17}\cdot 0.246,\mathrm{s}=878.5,\mathrm{s}$ against the PDG value $878.4,\mathrm{s}$, marked RS_PASS as a structural theorem (zero sorry, zero axiom). The local cost object is a two-argument domain cost on reals (mass and energy style inputs), built from the imported Cost layer whose one-argument $J$-cost is nonnegative on positive states.
Upstream, ObserverForcing already states that every recognition event has nonnegative cost via $J$-cost nonnegativity at positive state. The certificate lifts that nonnegativity idea to the module's two-argument domain cost, adds a diagonal vanishing condition (zero self-mismatch), and requires the module's canonical threshold to be positive so comparison cuts sit above zero.
Sibling lemmas in the same file discharge the three fields: diagonal identity, domain-cost nonnegativity under positive arguments, and positivity of the canonical threshold.
proof idea
No proof body: this is a structure whose fields are propositions. Inhabitation is deferred. The downstream definition cert fills the three fields by the sibling lemmas for diagonal vanishing, domain-cost nonnegativity, and threshold positivity. cert_inhabited is then the one-line Nonempty witness ⟨cert⟩.
why it matters
Gives a single named interface that Module 3's neutron-lifetime structural package must satisfy before the concrete certificate is assembled. Parents are the concrete inhabitant and the nonempty theorem in the same module; those close the STRUCTURAL THEOREM status advertised in the module header (PDG-level lifetime match via $\phi^{17}$ scaling).
In the broader RS stack this sits under the Cost/$J$ layer (T5 $J$-uniqueness and nonnegativity of recognition cost) rather than under the forcing chain's geometric steps (eight-tick, $D=3$). It does not itself derive the lifetime formula; it packages the cost and threshold hygiene that the module treats as prerequisite structure for the RS_PASS claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.