RSPhysics004Cert
plain-language theorem explainer
Certificate bundle for Physics Module 4 (Weinberg angle tree formula): diagonal vanishing of the domain cost, nonnegativity of that cost on positive arguments, and positivity of the canonical threshold. Downstream code builds a concrete inhabitant and a Nonempty proof from sibling lemmas. Pure structure definition; no proof body.
Claim. A Module-4 physics certificate is a triple of properties: (1) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (2) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
Physics RS Module 4 records the tree-level Weinberg angle identity $\sin^2\theta_W = J(\phi)/(1+J(\phi)) \approx 0.1054$, with a stated loop-corrected value near $0.231$. The module is marked structural (zero sorry, zero axiom).
The certificate packages three elementary cost facts used as local hygiene for that derivation. Domain cost is the module's bivariate cost on real arguments (mass/energy-style pairs in the sibling defs). It is expected to vanish on the diagonal $m=e$ away from zero and to stay nonnegative when both arguments are positive, mirroring the global J-cost nonnegativity from ObserverForcing ("the cost of any recognition event is non-negative").
The third field only asserts that the module's canonical threshold is positive, so later comparisons against that cutoff are well-posed.
proof idea
No proof: this is a structure whose fields are propositions. Inhabitation is deferred to the sibling cert, which fills the three fields by the lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The upstream cost_nonneg on recognition events supplies the conceptual template (J-cost nonnegativity) that the domain-cost nonnegativity field echoes.
why it matters
Gives a single named type for the cost/threshold side conditions of Module 4 so the module can export one inhabited certificate rather than three loose lemmas. Downstream, cert assembles the instance and cert_inhabited proves Nonempty of the structure, closing the module's structural-theorem claim.
In the broader RS stack this sits under the J-cost uniqueness (T5) and the golden-ratio fixed point $\phi$ (T6): the Weinberg tree formula is written directly in $J(\phi)$. The certificate itself does not derive $\sin^2\theta_W$; it only standardizes the cost positivity and diagonal-minimum facts the module treats as prerequisites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.