cert
plain-language theorem explainer
Packages three elementary properties of the module-4 domain cost and threshold into one certificate record for the Weinberg-angle physics module. Anyone citing the structural status of RS Physics Module 4 (tree-level sin²θ_W from J(φ)) uses this bundle. The definition is a pure structure inhabitant: it wires three already-proved sibling lemmas into the certificate fields.
Claim. There is a certificate consisting of: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 4 treats the Weinberg angle at tree level via the Recognition cost: $\sin^2\theta_W = J(\varphi)/(1+J(\varphi)) \approx 0.1054$, with a loop-corrected target near $0.231$. The module is marked structural (zero sorry, zero axiom).
The certificate structure RSPhysics004Cert packages three side conditions on a two-argument domain cost and a positive threshold. Domain cost is the local cost functional used in this module; its diagonal vanishing and nonnegativity mirror the global J-cost facts from ObserverForcing ("The cost of any recognition event is non-negative"), specialized to positive real mass/energy arguments. The canonical threshold is the positive cutoff against which that cost is compared.
Upstream, nonnegativity of recognition cost is already established via Cost.Jcost_nonneg on events with positive state.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional reasoning: the definition is just the record assembly of those three proofs.
why it matters
Gives the module a single named certificate object that asserts the cost/threshold hygiene needed before quoting the tree-level Weinberg formula $\sin^2\theta_W = J(\varphi)/(1+J(\varphi))$. In the Recognition chain this sits downstream of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the forced golden ratio $\varphi$ (T6), since the numerical value is read off $J(\varphi)$. No downstream consumers are wired yet in the graph; the sibling cert_inhabited is the natural next step that witnesses non-emptiness of the certificate type. Closes the local "certificate exists" obligation for a STRUCTURAL THEOREM module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.