IndisputableMonolith.Constants.FermiConstantScoreCard
Scorecard module for the Fermi constant G_F in GeV^{-2}: an RS structural prediction is bracketed against the CODATA reference value. Anyone checking electroweak or weak-rate numerics in the constants registry cites it. The argument builds a closed-form prediction from the electroweak VEV and w8 gap weight, proves positivity of the denominator, and certifies that CODATA lies inside the predicted interval.
claimIn natural units (GeV$^{-2}$), the RS Fermi-constant prediction $G_F^{\mathrm{pred}}$ is formed from the electroweak VEV structure and the eight-tick gap weight $w_8$. The module supplies lower and upper bounds on that prediction, records the CODATA reference $G_F^{\mathrm{CODATA}}$, and certifies $G_F^{\mathrm{CODATA}} \in [G_F^{\mathrm{pred,lo}}, G_F^{\mathrm{pred,hi}}]$.
background
Recognition Science treats dimensionful constants as derived from the phi-ladder and structural gap weights rather than free inputs. The Fermi constant $G_F$ sets the strength of the four-fermion weak interaction; in natural units it is tied to the electroweak vacuum expectation value by $G_F = 1/(\sqrt{2}, v^2)$ (up to the precise RS packaging used here).
Upstream, ElectroweakVEVStructure formalizes registry item C-020: what fixes $v \approx 246,\mathrm{GeV}$. The numerical gap weight $w_8$ from the eight-tick construction enters as the closed form $w_8 = (348 + 210\sqrt{2} - (204 + 130\sqrt{2})\varphi)/7$, with certified interval bounds from W8Bounds (approximately $2.490569$).
This module is the P1-C01 scorecard: predicted row, CODATA row, equality/identity lemmas for the prediction formula, positivity facts needed for division, and a bracket certificate that the reference value sits inside the predicted window.
proof idea
Definition-and-certificate layout, not a single deep theorem. Prediction and CODATA rows are recorded as concrete real expressions. Positivity of $\sqrt{2}$ and of the Fermi denominator discharge well-definedness of the closed form. Interval arithmetic (via the imported $w_8$ bounds and VEV structure) yields lower and upper edges for the prediction; a bracket lemma packages those edges. The main certificate then checks that the CODATA value lies in that interval and packages the whole scorecard as a single Prop that holds by the preceding inequalities.
why it matters in Recognition Science
Closes the constants-registry entry for $G_F$ so downstream weak-rate numerics can cite a certified prediction rather than an external fit. The immediate consumer is the dark-matter weak neutrino-reference cross-section scorecard (P0-A6), whose reference channel is $\sigma_{\nu,\mathrm{ref}} = G_F^2 E_{\mathrm{ref}}^2$ after unit conversion GeV$^{-2}\to\mathrm{cm}^2$. Without a bracketed $G_F$, that cross-section row cannot be scored inside the RS ledger.
In the broader forcing picture the module sits on the electroweak side of the constants layer: VEV structure plus eight-tick $w_8$ feed $G_F$, which then anchors weak interaction normalizations used across particle-physics scorecards. It does not itself re-derive $v$ or $w_8$; it consumes those modules and emits the Fermi scorecard certificate.
scope and limits
- Does not derive the electroweak VEV from first principles; imports that structure.
- Does not re-prove the closed form or interval bounds for the eight-tick weight w8.
- Does not claim a unique microscopic mechanism beyond the RS structural formula used.
- Does not convert units or evaluate weak cross sections; only supplies G_F numerics.
- Does not address running of G_F or higher-order electroweak corrections.
used by (1)
depends on (2)
declarations in this module (11)
-
def
row_fermi_pred -
def
row_fermi_codata -
theorem
row_fermi_pred_eq -
theorem
sqrt2_pos -
theorem
fermi_den_pos -
theorem
row_fermi_pred_lower -
theorem
row_fermi_pred_upper -
theorem
row_fermi_pred_bracket -
theorem
row_fermi_codata_in_bracket -
structure
FermiConstantScoreCardCert -
theorem
fermiConstantScoreCardCert_holds