RSPhysics011Cert
plain-language theorem explainer
Certificate bundle for Physics Module 11 (Z-boson mass match): diagonal domain cost vanishes, domain cost is nonnegative on positive mass/energy, and the canonical threshold is positive. Downstream code cites it to inhabit a structural zero-sorry certificate. The declaration is a pure structure interface; proofs live in the field witnesses.
Claim. A certificate is a triple of properties: (i) for every real $r \neq 0$, the domain cost at equal arguments vanishes, $\mathrm{domainCost}(r,r)=0$; (ii) for all $m,e>0$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 11 records the Z-boson mass match $M_Z \approx 91.2,\mathrm{GeV} \sim \varphi^{13}\cdot 0.175$, marked as a structural theorem (zero sorry, zero axiom). The local cost object is a two-argument domain cost on reals (mass and energy scales), together with a positive canonical threshold used as a cutoff in the module.
Recognition Science costs descend from the J-cost $J(x)=(x+x^{-1})/2-1$, forced unique by the Recognition Composition Law. Upstream, ObserverForcing already proves that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states. The three fields here specialize that nonnegativity and the on-diagonal vanishing to the module's domain cost, and pin positivity of the threshold used in the mass-ladder comparison.
proof idea
No proof body: this is a structure definition packing three Prop fields. Inhabitation is deferred to the sibling cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos fieldwise. Those lemmas (not this declaration) carry the actual arguments, drawing on the global $J$-cost nonnegativity pattern from ObserverForcing.
why it matters
Gives Module 11 a single named certificate type so the Z-mass structural claim can be discharged as Nonempty RSPhysics011Cert via cert_inhabited. Downstream cert is the concrete witness; cert_inhabited packages it for any consumer that only needs existence.
In the broader RS ladder, Z sits near rung scale $\varphi^{13}$ with the yardstick mass formula. The certificate does not itself compute $M_Z$; it only locks the cost/threshold hygiene the module treats as prerequisite for calling the numerical match structural. Ties to the phi-ladder and T5/T6 J-uniqueness and self-similar fixed point only indirectly, through the cost axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.