cert
plain-language theorem explainer
Packages the Module-7 certificate: domain cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is positive. Anyone citing the top-Yukawa structural claim (y_t = 1 at unification, top as the φ^0 rung) uses this bundle. Proof is a three-field structure instance wiring already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 7 treats the top Yukawa as structural: $y_t = 1$ at unification, with the top quark sitting at the $\phi^0 = 1$ coupling on the Recognition ladder. Status is a structural theorem (no sorry, no axioms).
The certificate structure bundles three cost-side facts about domainCost (the module's cost functional on mass/energy pairs) and canonicalThreshold (the positive cutoff used in the module). Diagonal vanishing says equal nonzero arguments incur zero cost; non-negativity is the usual Recognition cost lower bound; threshold positivity keeps the cutoff well-defined.
Upstream, ObserverForcing already records that every recognition event has non-negative cost via $J$-cost non-negativity. The module reuses that spirit for its domain cost lemmas, then packages them here.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra; pure packaging.
why it matters
Gives a single named inhabitant of the Module-7 certificate so downstream physics code can assume the cost axioms without reopening the three lemmas. It sits under the structural claim that the top Yukawa is unity at unification and that the top is the $\phi^0$ rung on the phi-ladder (primer: T6 forces $\phi$ as the self-similar fixed point; mass/coupling rungs live on that ladder).
No used_by edges are recorded yet; the sibling cert_inhabited is the natural consumer. The declaration closes the certificate interface for this module rather than proving a new dynamical identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.