WZBosonRatioScoreCardCert
plain-language theorem explainer
The declaration defines a structure that bundles two interval certificates: the W/Z mass ratio from PDG inputs lies in (0.87, 0.89) and sin²θ_W lies in (0.22, 0.23). Particle physicists auditing Standard Model parameters against Recognition Science predictions would cite it as a numeric interface. The definition simply packages the two bounds with no further computation or derivation.
Claim. Let $r = m_W/m_Z$ be the ratio computed from the PDG values $m_W = 80.377$ GeV and $m_Z = 91.1876$ GeV. The structure asserts $0.87 < r < 0.89$ together with $0.22 < 1 - r^2 < 0.23$.
background
In Recognition Science the W/Z ratio is predicted by the GaugeBosonMassesFromRS definition massRatio := 6/(3 + phi). The present module supplies a data-interface certificate that records the experimental interval for that ratio and for the derived Weinberg angle. Upstream StandardModel.WZMassRatio provides the concrete massRatio and sin2ThetaW functions whose values are taken directly from the PDG pair; the module doc states that the stated bounds are algebraic consequences of those input definitions. The local setting is Phase 2 P2-WZ, which treats the PDG masses as fixed external data rather than deriving them from the phi-ladder or the forcing chain.
proof idea
The declaration is a bare structure definition with an empty proof body. It functions as a data-interface certificate that simply records the two interval facts supplied by the sibling row functions row_WZ_ratio_bracket and row_sin2_from_WZ_masses.
why it matters
The structure is instantiated by the downstream theorem wzBosonRatioScoreCardCert_holds, which constructs a witness using the row functions. It supplies the numeric bounds required for the WZ sector in the Recognition Science mirror while the RS-native formula sin²θ_W = (3 - phi)/6 is proved separately in Q3Representations. The certificate therefore closes the data-interface step for the eight-tick octave and D = 3 predictions without addressing the open matching question between the phi-based formula and the PDG interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.