row_fermi_pred
plain-language theorem explainer
The row_fermi_pred definition supplies the Recognition Science prediction for the Fermi constant in natural units as the reciprocal of sqrt(2) times the square of the canonical electroweak VEV. Electroweak precision physicists checking consistency with CODATA data would cite this when verifying the interval (1.16e-5, 1.17e-5) GeV^{-2}. It is realized as a direct noncomputable real definition that substitutes the fixed VEV value of 246 GeV.
Claim. The predicted Fermi constant satisfies $G_F = 1/ (√2 v^2)$ where $v = 246$ GeV is the canonical electroweak vacuum expectation value.
background
This declaration belongs to the Fermi Constant Score Card module implementing Phase 1 row P1-C01. The module encodes the natural-unit electroweak identity $G_F = 1/(√2 v^2)$ together with the canonical RS electroweak VEV surface. The measurement target is the CODATA/PDG value $G_F = 1.1663787 × 10^{-5}$ GeV^{-2}, with the RS prediction required to lie inside the bracket (1.16 × 10^{-5}, 1.17 × 10^{-5}).
proof idea
The definition is a direct algebraic expression substituting the canonical VEV into the standard electroweak formula. Downstream interval theorems unfold the definition and apply real-number inequalities on the denominator.
why it matters
The definition populates the FermiConstantScoreCardCert structure that certifies the CODATA value lies inside the RS bracket. It fills the P1-C01 slot in the physical derivation plan and supplies the Fermi bracket used by the dark-matter weak-reference cross-section scorecard. The row remains partial because the full SI/GeV VEV bridge is still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.