RSPhysics007Cert
plain-language theorem explainer
Certificate bundle for Physics Module 7 (top Yukawa at unification): diagonal domain cost vanishes, domain cost is nonnegative on positive mass/energy, and the canonical threshold is positive. Anyone assembling or inhabiting the Module 7 certificate cites this. Pure structure definition; the three fields are discharged by sibling lemmas in the same module.
Claim. A Module-7 certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) whenever mass $m>0$ and energy $e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 7 encodes the structural claim that the top Yukawa equals one at unification: the top quark sits at the $\phi^0=1$ coupling on the Recognition ladder. The module is marked as a structural theorem (zero sorry, zero axiom).
Domain cost is the local cost functional on mass/energy pairs used in this module; the diagonal identity $C(r,r)=0$ for $r\neq 0$ says matched arguments carry no excess cost. Nonnegativity for positive mass and energy is the physics-side shadow of the foundation fact that every recognition event has nonnegative cost (via $J$-cost nonnegativity). The canonical threshold is the positive cutoff against which the top coupling is compared.
Upstream, ObserverForcing records that the cost of any recognition event is nonnegative, grounded in $J$-cost nonnegativity at positive state.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Inhabitation is deferred to the sibling definition cert, which fills them by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. cert_inhabited then packages that witness as Nonempty.
why it matters
This structure is the typed interface for Module 7's top-Yukawa certificate. Downstream, cert builds a concrete inhabitant and cert_inhabited proves the type is nonempty, closing the structural theorem that $y_t=1$ at unification with the top as the $\phi^0=1$ coupling.
In the broader Recognition chain, the claim sits on the $\phi$-ladder mass/coupling organization (T6 forces $\phi$ as the self-similar fixed point) and on cost nonnegativity from the $J$-cost calculus (T5). It does not itself derive the numerical Yukawa; it packages the cost and threshold hygiene needed before that identification is used elsewhere in the physics modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.