FermiConstantScoreCardCert
plain-language theorem explainer
The FermiConstantScoreCardCert structure records three interval assertions: the RS-computed Fermi constant lies inside (1.16e-5, 1.17e-5) GeV^{-2}, the CODATA value does likewise, and the canonical electroweak VEV sits inside (244, 248) GeV. A physicist checking electroweak constants against Recognition Science predictions would cite this certificate for the P1-C01 row. It is introduced as a plain record definition whose fields are the three required real-number inequalities.
Claim. The certificate structure asserts that the predicted Fermi constant satisfies $1.16times10^{-5} < 1/(sqrt{2}v^2) < 1.17times10^{-5}$ (in GeV$^{-2}$), the CODATA value $1.1663787times10^{-5}$ lies in the same open interval, and the canonical VEV obeys $244 < v < 248$ (in GeV).
background
The Fermi Constant Score Card module evaluates the natural-unit electroweak identity $G_F = 1/(sqrt{2} v^2)$ at the canonical RS VEV. Upstream, vev_canonical supplies the fixed value 246, row_fermi_pred computes the reciprocal expression $1/(sqrt{2} vev_canonical^2)$, and row_fermi_codata stores the measured 1.1663787e-5. The module targets the bracket (1.16e-5, 1.17e-5) GeV^{-2} so that both the RS prediction and the CODATA datum fall inside it.
proof idea
The declaration is a structure definition that directly enumerates the three field names together with their inequality types. No lemmas or tactics are invoked; the body is empty because the declaration only specifies the record layout. The fields simply reference the sibling definitions row_fermi_pred, row_fermi_codata and the imported vev_canonical.
why it matters
This structure supplies the certificate object consumed by the downstream theorem fermiConstantScoreCardCert_holds, which proves the structure is inhabited. It implements Phase 1 row P1-C01 of the physical derivation plan for the Fermi constant. The result supports the claim that RS predictions recover the electroweak scale inside the observed interval; the remaining open question is the derivation of the 246 GeV VEV from the phi-ladder or forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.