cert
plain-language theorem explainer
Packages the three structural obligations for the RS top-Yukawa certificate into one inhabited record: diagonal domain cost vanishes, domain cost is nonnegative off-diagonal, and the canonical threshold is positive. Anyone citing the Higgs-coupling structural theorem uses this witness. The body is a three-field structure instance wiring existing local lemmas.
Claim. There is a certificate record asserting: (i) for every $r \neq 0$, the domain cost of the pair $(r,r)$ is zero; (ii) for all $m,e > 0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive. These three facts are the structural content of the RS claim that the top Yukawa sits at unity on the $\varphi^6$ rung.
background
The module treats the top Yukawa $y_t = \sqrt{2}, m_t/v \approx 0.994 \sim 1$ as an RS structural identity: at the $\varphi^6$ rung one has $y_t = 1$, matching the Planck-scale unification value. The certificate is not a numerical fit; it packages cost-theoretic side conditions that make that identity well-posed.
domainCost is the local cost functional on mass/energy pairs used in this module. The structure HiggsCouplingCert demands three properties of that cost and of a fixed positive threshold: vanishing on the diagonal (equal arguments), nonnegativity for positive arguments, and positivity of the threshold. Upstream, the foundation lemma cost_nonneg records that every recognition-event cost is nonnegative via $J$-cost nonnegativity; the local lemmas domainCost_nonneg and domainCost_at_eq specialize that idea to the Higgs-coupling domain cost.
proof idea
One-line structure instance. The three fields of HiggsCouplingCert are filled by the already-proved local facts domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new algebra is performed; the definition is pure packaging of those three lemmas into a single certificate value.
why it matters
Gives a single named witness that the RS top-Yukawa structural claim is certificate-complete: diagonal cost zero, cost nonnegative, threshold positive. The module presents this as a structural theorem (zero sorry, zero axiom) supporting $y_t = 1$ at the $\varphi^6$ rung, consistent with the observed $y_t \approx 1$ and with unification-scale top Yukawa equal to one. No downstream consumers are wired yet in the graph; the natural parent is any theorem that assumes an inhabited HiggsCouplingCert (e.g. cert_inhabited). Landmark contact is the phi-ladder mass/coupling placement rather than T5–T8 forcing itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.