row_fermi_codata_in_bracket
plain-language theorem explainer
The theorem verifies that the Recognition Science Fermi constant value 1.1663787e-5 lies strictly inside the interval (1.16e-5, 1.17e-5) in GeV^{-2}. Electroweak phenomenologists comparing RS predictions to PDG data would cite the result to confirm bracket consistency for the G_F parameter. The proof is a direct numerical check that unfolds the constant definition and normalizes both sides of the conjunction.
Claim. $1.16times10^{-5} < G_F^{RS} < 1.17times10^{-5}$ where $G_F^{RS}$ is the Recognition Science Fermi constant in GeV^{-2} obtained from the electroweak identity with canonical VEV 246 GeV.
background
The Fermi Constant Score Card module implements Phase 1 row P1-C01 of the physical derivation plan. It encodes the natural-unit identity $G_F = 1/(sqrt{2} v^2)$ with the canonical electroweak VEV $v=246$ GeV and targets the CODATA/PDG measurement $G_F=1.1663787times10^{-5}$ GeV^{-2}. The upstream definition row_fermi_codata supplies this measured value directly as a real number for the bracket test.
proof idea
The term-mode proof unfolds row_fermi_codata to expose the literal 1.1663787e-5, then applies constructor to split the conjunction and norm_num to discharge both inequalities by direct numerical comparison.
why it matters
The result supplies the codata_in_bracket field required by fermiConstantScoreCardCert_holds to build the nonempty FermiConstantScoreCardCert. It closes the numerical consistency check for the electroweak sector, confirming that the RS prediction brackets the measured G_F. The module remains partial pending the full SI/GeV VEV bridge from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.