cert
plain-language theorem explainer
Packages a three-field certificate that the muon-mass domain cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and that the canonical threshold is positive. Anyone invoking the MuonMass3v2Cert interface cites this inhabitant. Proof is pure field packing of three already-proved sibling lemmas.
Claim. There is an inhabitant of the muon-mass certificate structure witnessing: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive mass $m$ and energy $e$, the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module targets a structural account of the muon mass on the Recognition Science phi-ladder (Plan v7, 118th pass). The experimental anchor is $m_\mu \approx 105.66,\mathrm{MeV}$; the module notes that naive rung placements such as $\phi^{11} E_{\mathrm{coh}}$ still miss the number, so the present layer is structural rather than numerical.
The certificate structure MuonMass3v2Cert packages three Prop fields about a real-valued domain cost: diagonal vanishing, nonnegativity on the positive quadrant, and positivity of a canonical threshold. Upstream, the foundation lemma cost_nonneg states that the cost of any recognition event is nonnegative, via nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$ for $x>0$. The local domain-cost lemmas specialize that idea to the muon-mass comparison.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new arithmetic is performed; the def only witnesses that those three facts inhabit the certificate record.
why it matters
Gives a single named certificate object for the structural muon-mass layer on the phi-ladder, so downstream mass or gap arguments can assume one record rather than three separate lemmas. Fits the RS mass pattern (yardstick times a phi-power with rung and gap corrections) while remaining honest that the numerical MeV value is not yet forced. No used_by edges are recorded yet; the sibling cert_inhabited is the natural next consumer. Touches the broader forcing chain only indirectly through J-cost nonnegativity (T5 landmark), not through T6–T8 dimension or octave claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.