IndisputableMonolith.Constants.FermiConstantScoreCard
The FermiConstantScoreCard module assembles the RS prediction for the Fermi constant in GeV^{-2} units by combining the electroweak VEV structure with the closed-form eight-tick weight w8. Particle physicists modeling weak interactions or neutrino cross sections cite it for consistency with codata. The module structures the argument as a sequence of row definitions for predicted and measured values, positivity lemmas, and a final certification theorem that places the prediction inside explicit numerical bounds.
claimThe RS prediction for the Fermi constant $G_F$ (in GeV$^{-2}$) satisfies the bracketed interval derived from the electroweak vacuum expectation value $v$ and the eight-tick weight $w_8 = (348 + 210√2 - (204 + 130√2)φ)/7$, with the certification establishing that the predicted row lies inside the codata bounds.
background
The module imports the electroweak VEV structure, which formalizes the RS framework for determining the vacuum expectation value $v ≈ 246$ GeV, and the W8 numerical bounds module, which supplies the parameter-free closed form $w_8 = (348 + 210√2 - (204 + 130√2)φ)/7 ≈ 2.490569$. It defines a scorecard consisting of row definitions for the predicted Fermi constant, the corresponding codata entry, their equality under the model, positivity statements, and lower/upper bounds that together produce a certified bracket. This construction lives inside the constants domain and draws directly on the eight-tick octave (T7) and the phi-ladder mass formula.
proof idea
This is a definition module that organizes the Fermi constant scorecard through a series of row definitions, positivity lemmas, and a terminal certification theorem. It applies the imported VEV structure and W8 closed-form bounds to establish the prediction interval; the certification theorem is a one-line wrapper that invokes the bracket lemma on the predicted and codata rows.
why it matters in Recognition Science
The module supplies the P1-C01 Fermi constant prediction that is imported by the DarkMatterWeakReferenceCrossSectionScoreCard to compute the weak neutrino-reference cross section via $σ_{ν ref} = G_F^2 E_{ref}^2$ (with unit conversion). It advances the Recognition Science constants chain by delivering a certified numerical bracket consistent with the phi-ladder and the eight-tick weight, closing one link in the T5–T8 forcing sequence.
scope and limits
- Does not derive the Fermi constant from the full T0–T8 forcing chain.
- Does not perform unit conversions outside GeV^{-2}.
- Does not incorporate higher-order radiative corrections.
- Does not compare the prediction against experimental data beyond the supplied codata row.
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