cert
plain-language theorem explainer
Packages three elementary facts about the RS5 domain cost and threshold into a single Weinberg-angle certificate: diagonal cost vanishes, cost is nonnegative on positive arguments, and the canonical threshold is positive. Cited by anyone assembling the structural RS5 Weinberg package. The definition is a pure field-assembly of three already-proved lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical threshold is strictly positive.
background
The module treats the electroweak mixing angle in Recognition Science units. The PDG value is $\sin^2\theta_W\approx 0.2312$. The bare RS ladder identity $1-M_W^2/M_Z^2=1-\varphi^{24}/\varphi^{25}=1-\varphi^{-1}\approx 0.382$ is read as a GUT-scale structural value that must run down to the $M_Z$ scale; the module is marked as a structural theorem with no sorry and no extra axioms.
domainCost is the local cost functional on pairs of positive reals used in this RS5 session. The certificate structure WeinbergAngle5Cert demands three properties of that cost and of a fixed positive threshold: vanishing on the diagonal away from zero, nonnegativity for positive arguments, and positivity of the threshold. Upstream, the general recognition-event cost is already known to be nonnegative via the J-cost minimum at $x=1$ (cost_nonneg in ObserverForcing).
proof idea
One-line structure inhabitant. The three fields of WeinbergAngle5Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further rewriting or case analysis occurs.
why it matters
Gives a single inhabited certificate object for the RS5 Weinberg-angle structural layer, so downstream code can depend on one name rather than three separate lemmas. The module frames the bare RS value $1-\varphi^{-1}\approx 0.382$ as the GUT-scale fixed point (linked to the phi-ladder and T6 self-similarity), with the experimental $0.2312$ understood as the result of running to the $Z$ pole. No parent theorems currently consume this certificate (used_by is empty), but the sibling cert_inhabited and any future running or matching lemmas are the natural consumers. It does not close the numerical gap to PDG; it only packages the cost/threshold side conditions of the structural story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.