cert
plain-language theorem explainer
Packages three structural facts about the domain J-cost into a single Higgs-decay-width certificate: vanishing on the diagonal, non-negativity off the diagonal, and a positive canonical threshold. Anyone citing the cubic J-cost model of Γ_H would reach for this inhabitant. The body is a pure structure assembly of three already-proved field lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ is strictly positive.
background
The module studies a structural (not numerical) model of the Higgs total width from the Recognition Science J-cost. The classical RS guess $\Gamma_H=J(\varphi)M_H$ overshoots experiment by thousands; the cubic trial $\Gamma_H=J(\varphi)^3 M_H$ is closer but still off. The present file therefore isolates only the algebraic skeleton that any such model must obey.
Domain cost is the two-argument cost used on mass/energy pairs; its diagonal vanishing and off-diagonal non-negativity are the minimal positivity axioms inherited from the global J-cost $J(x)=(x+x^{-1})/2-1$. The canonical threshold is the positive scale against which a decay channel is declared open. Upstream, cost_nonneg already records that every recognition event has non-negative cost via $J\ge 0$.
proof idea
One-line structure inhabitant. The three fields of HiggsDecayWidth3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further rewriting or case analysis occurs.
why it matters
Gives a single named witness that the cubic J-cost Higgs-width skeleton is inhabited, so later numerical or forcing arguments can assume the three axioms by projecting out of this certificate rather than re-proving them. The module is marked structural (0 sorry, 0 axiom) and sits in the physics layer that tries to recover $\Gamma_H\approx 4.07,\mathrm{MeV}$ from powers of $J(\varphi)$ and $M_H$. No downstream consumers are wired yet; the immediate sibling cert_inhabited is the natural next step that turns the definition into a inhabited-type fact. Touches the broader RS program of deriving particle widths from the unique J forced at T5 and the golden ratio fixed at T6, without yet closing the numerical gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.