BosonVerificationCert
plain-language theorem explainer
BosonVerificationCert bundles the phi-derived Weinberg angle bounds, the WZ mass ratio equality, and the electroweak sector offsets into a single record. Particle physicists checking consistency of the phi-ladder mass formula against PDG values would cite it when confirming the electroweak sector. The structure is assembled directly from the module's angle definitions and the Anchor sector parameters.
Claim. A certificate requiring $0.2302 < (3 - φ)/6 < 0.2304$, $0.7696 < 1 - (3 - φ)/6 < 0.7698$, $(3 + φ)/6 = 1 - (3 - φ)/6$, $B_φ(Electroweak) = 1$, and $r_0(Electroweak) = 55$.
background
The module supplies machine-verified electroweak boson mass predictions on the phi-ladder. Experimental inputs remain quarantined constants; the RS formula for the sector is m(EW, r) = 2 φ^{50+r} / 10^6 MeV. The Weinberg angle is defined as sin²θ_W = (3 - φ)/6, which yields cos²θ_W = 1 - sin²θ_W and the squared mass ratio (3 + φ)/6. B_pow and r0 are sector-specific constants: B_pow(Electroweak) = 1 and r0(Electroweak) = 55. Upstream states that these offsets are derived from cube edge counting and wallpaper-plus-cube geometry, respectively, and are not arbitrary.
proof idea
The declaration is a structure definition whose four fields are populated directly from the sibling definitions sin2_theta_W, cos2_theta_W, wz_mass_ratio_sq, B_pow, and r0 together with the explicit numerical bounds.
why it matters
The certificate is the concrete witness supplied to the downstream theorem boson_verification_cert_exists, which proves Nonempty BosonVerificationCert. It therefore closes the verification step for the electroweak sector inside the Recognition Science mass predictions, confirming that the phi-derived angle lies inside the stated experimental window while the geometric sector parameters B_pow = 1 and r0 = 55 are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.