row_fermi_pred_upper
plain-language theorem explainer
The theorem establishes that the Recognition Science prediction for the Fermi constant, computed as the reciprocal of sqrt(2) times the square of the canonical 246 GeV vacuum expectation value, lies strictly below 1.17 times 10 to the minus five in GeV inverse squared. Electroweak precision analyses would cite this bound when checking consistency between the RS-derived interval and CODATA data. The proof unfolds the prediction definition, rewrites via a division inequality using denominator positivity, inserts the decimal lower bound on sqrt(2)
Claim. Let $G_F = 1/ (sqrt(2) v^2)$ with canonical vacuum expectation value $v = 246$ GeV. Then $G_F < 1.17 times 10^{-5}$ in GeV^{-2}.
background
The Fermi Constant Score Card module treats Phase 1 row P1-C01 of the physical derivation plan. It implements the natural-unit electroweak identity $G_F = 1/(sqrt(2) v^2)$ using the canonical RS electroweak VEV surface $v = 246$ GeV. The definition of the predicted Fermi constant is exactly this reciprocal expression. The module proves the interval $1.16 times 10^{-5} < G_F < 1.17 times 10^{-5}$ so that the CODATA value lies inside the bracket. Upstream results supply the definition of the canonical VEV as exactly 246, the positivity theorem for the denominator sqrt(2) times VEV squared, the lower decimal bound 1.4142 less than sqrt(2), and the definition of the prediction itself.
proof idea
The proof unfolds the definition of the predicted Fermi constant. It rewrites the target inequality using the division rule justified by the positivity theorem for the denominator. A hypothesis records that 1.4142 is less than sqrt(2). A second hypothesis establishes that the approximate denominator using 1.4142 and 246 is strictly less than the exact denominator, obtained by reflexivity on the VEV value followed by nonlinear arithmetic. A numerical check verifies that 1 is less than the product of the target bound and the approximate denominator. Nonlinear arithmetic closes the argument.
why it matters
This upper bound is the second half of the bracket theorem that asserts the full interval around the predicted Fermi constant. The bracket theorem in turn fills Phase 1 row P1-C01 by showing that the CODATA measurement sits inside the RS-computed range. The result rests on the natural-unit identity $G_F = 1/(sqrt(2) v^2)$ together with the canonical VEV of 246 GeV. It leaves open the full derivation of the VEV scale from the Recognition Science forcing chain and the SI/GeV bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.