cert
plain-language theorem explainer
Packages three elementary properties of the seesaw domain cost into a single certificate: diagonal vanishing, nonnegativity for positive mass/energy, and a positive canonical threshold. Anyone citing the RS v3 seesaw structural theorem uses this witness. The body is a pure structure assembly from three sibling lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module formalizes the RS seesaw mechanism as a structural theorem (zero sorry, zero axioms). Physically, the classical seesaw is $m_\nu\sim m_D^2/M_R$ with $M_R$ at the GUT scale, giving a rough RS estimate $m_\nu\sim m_{\mathrm{top}}^2/M_{\mathrm{GUT}}\approx 1.5\times 10^{-3},\mathrm{eV}$ against an empirical scale $\sim 0.05,\mathrm{eV}$.
The certificate structure bundles three cost axioms on a real bivariate domain cost: it vanishes when the two arguments coincide (and are nonzero), stays nonnegative on the positive quadrant, and admits a strictly positive canonical threshold. Nonnegativity of recognition cost is the ambient prior from ObserverForcing: "The cost of any recognition event is non-negative," proved via $J$-cost nonnegativity.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional rewriting or case analysis occurs.
why it matters
Gives an inhabited certificate for the RS v3 seesaw structural layer, so downstream arguments can assume diagonal vanishing, cost nonnegativity, and a positive threshold without re-proving them. The module status line marks this as a structural theorem with no sorry and no axioms; the certificate is the concrete witness that status refers to. It sits in Foundation alongside the forcing chain and cost calculus, and supports the seesaw mass estimate narrative ($M_R\sim M_{\mathrm{GUT}}$, $m_\nu\sim m_t^2/M_{\mathrm{GUT}}$) without claiming a precision fit to the observed $0.05,\mathrm{eV}$ scale. No used-by edges are recorded yet; the natural consumer is any lemma that needs a SeesawMech_RS_v3Cert instance (e.g. inhabitedness).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.