row_fermi_codata
plain-language theorem explainer
The definition supplies the CODATA/PDG experimental value of the Fermi constant G_F equal to 1.1663787 times 10 to the minus five in units of GeV inverse squared. A physicist comparing Recognition Science electroweak predictions to particle data would cite this entry when confirming that the measured value lies inside the derived interval. It is introduced by direct numeric assignment with no reduction steps.
Claim. The CODATA value of the Fermi constant is $G_F = 1.1663787 × 10^{-5} GeV^{-2}$.
background
This module treats the Fermi constant as phase 1 row P1-C01. The target identity is the electroweak relation G_F = 1 / (sqrt(2) * v^2) with canonical VEV v = 246 GeV. The module shows that the Recognition Science interval (1.16 × 10^{-5}, 1.17 × 10^{-5}) contains the measured value.
proof idea
The declaration is a direct numeric definition with no lemmas or tactics applied.
why it matters
It supplies the codata_in_bracket conjunct inside the FermiConstantScoreCardCert structure. This completes the scorecard comparison for the Fermi constant and links to the electroweak VEV structure at 246 GeV. The entry remains partial pending a full derived bridge from Recognition Science units to the canonical GeV scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.