cert
plain-language theorem explainer
Packages three elementary properties of the RS domain cost into a single certificate for the exact Weinberg-angle claim: diagonal vanishing, non-negativity on positive masses/energies, and a strictly positive canonical threshold. Anyone citing the exact-angle certificate in the Standard Model layer will use this witness. The body is a pure structure assembly of 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
This module sits in the Standard Model layer of Recognition Science and packages cost-side hypotheses used for an exact Weinberg-angle statement. The ambient cost is the RS J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain; the Recognition Composition Law constrains how costs compose under products and ratios.
Here a domain cost on pairs of real parameters (mass-like and energy-like) is the local object. The certificate structure demands three facts about it: the cost vanishes on the diagonal away from zero (equal arguments incur zero defect), it is non-negative for positive arguments, and a fixed positive threshold (the canonical acceptance cutoff) is available. Upstream, non-negativity of recognition-event cost is already known from ObserverForcing via $J$-cost non-negativity on positive states.
proof idea
One-line structure construction. The three fields of WeinbergAngleExactCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive inputs), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis occurs.
why it matters
Gives a single named witness that the cost side of the exact Weinberg-angle claim is inhabited, so downstream Standard Model arguments can assume diagonal zero cost, non-negative domain cost, and a positive threshold without re-proving each fact. It sits next to the inhabitedness lemma for the same certificate and is the natural handle for any exact-angle derivation that routes through domain-cost comparison to the canonical threshold. No used-by edges are recorded yet; the declaration is infrastructure for the RS exact-angle package rather than a numerical prediction of $\sin^2\theta_W$ itself. Framework landmarks in play are the T5 J-uniqueness of the cost and the non-negativity of recognition cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.