EWCert
plain-language theorem explainer
EWCert packages three numerical checks confirming the Recognition Science electroweak mass predictions. A physicist auditing the phi-ladder mass formulas would cite this certificate to verify that the Z prediction lies inside a 0.01 MeV window around 91.088 GeV and that the W/Z ratio reproduces the RS Weinberg angle. The structure is assembled directly from the interval, relative-error, and ratio lemmas already established in the same module.
Claim. An electroweak verification certificate consists of the three assertions that the predicted Z-boson mass $z_{pred}$ satisfies $91075.09 < z_{pred} < 91075.10$, that the relative deviation satisfies $|z_{pred} - m_{Z,exp}|/m_{Z,exp} < 0.0013$, and that the ratio of predicted W and Z masses equals the Recognition-Science value of the cosine of the Weinberg angle.
background
The ElectroweakMasses module assigns the Z boson to rung 1 of the phi-ladder in the electroweak sector, giving the explicit mass formula $m_Z = 2 φ^{51}/10^6$ MeV. The W mass is obtained from the gauge relation $m_W = m_Z cos θ_W$ where the RS prediction is $sin^2 θ_W = (3-φ)/6$ with zero free parameters. The structure EWCert collects the three concrete numerical checks that certify these formulas against experiment.
proof idea
EWCert is a structure definition with no proof body. It is instantiated in the downstream theorem ew_cert_exists by supplying the three facts z_mass_bounds for the interval condition, z_relative_error for the error bound, and wz_ratio_eq_cos for the ratio identity.
why it matters
This certificate is the object whose non-emptiness is asserted by ew_cert_exists, thereby confirming the electroweak mass predictions inside the Recognition Science framework. It directly implements the mechanism in the module documentation: Z at rung 1, W derived via the Weinberg angle from the phi-based $sin^2 θ_W$. The construction closes one verification step on the mass ladder before higher sectors are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.