row_fermi_pred_bracket
plain-language theorem explainer
The theorem shows that the Recognition Science Fermi constant prediction in natural units lies strictly between 1.16 times 10 to the minus 5 and 1.17 times 10 to the minus 5 GeV inverse squared. Electroweak precision tests and weak-interaction cross-section calculations would cite this bracket for consistency checks. The proof is a one-line term-mode constructor that pairs the independently established lower and upper bounds.
Claim. $1.16 times 10^{-5} < 1/(sqrt(2) v^2) < 1.17 times 10^{-5}$ (GeV^{-2}), where $v = 246$ GeV is the canonical electroweak vacuum expectation value.
background
The Fermi Constant Score Card module treats phase 1 row P1-C01 of the physical derivation plan. It encodes the tree-level electroweak identity G_F equals one over square root of two times v squared, with the canonical vacuum expectation value fixed at 246 GeV. The prediction is obtained by direct substitution of this value into the identity in natural units. The module establishes that the resulting number lies inside the open interval (1.16e-5, 1.17e-5) GeV^{-2}, which contains the CODATA/PDG central value. Upstream lower and upper bound theorems supply the two sides of the interval by applying explicit numerical bounds on sqrt(2) together with positivity of the denominator.
proof idea
The proof is a term-mode constructor that directly pairs the lower bound theorem with the upper bound theorem.
why it matters
This bracket certifies the Fermi constant scorecard and is imported into the dark matter weak reference cross section scorecard. It completes the P1-C01 entry by confirming that the RS electroweak prediction sits inside the experimental window. The parent certification theorem packages the bracket together with the codata comparison and VEV range check. An open question remains the derivation of the 246 GeV scale itself from the phi-ladder without canonical input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.