module module high

`IndisputableMonolith.Constants.FermiConstantScoreCard`

The module assembles a scorecard for the predicted Fermi constant in GeV^{-2} natural units under P1-C01. It combines the electroweak VEV framework with eight-tick numerical bounds to certify predicted and codata rows plus bracketing lemmas. Workers on weak-scale predictions or neutrino cross sections cite it for the G_F input to reference channels. The module is a collection of definitions and interval certificates with no internal proofs.

claim$G_F^{ m pred}$ in GeV$^{-2}$ units, with certified rows for prediction, codata, and bracketed interval derived from $v o G_F$ relation and $w_8$ weight.

background

The module sits in the constants domain and imports the ElectroweakVEVStructure (C-020) that formalizes the structural origin of the vacuum expectation value $v o 246$ GeV together with the W8Bounds module that supplies the closed-form gap weight $w_8 = (348 + 210\sqrt{2} - (204 + 130\sqrt{2})\phi)/7 \approx 2.490569$. These supply the inputs for the Fermi-constant rows. The local setting is the Recognition Science constants registry that expresses all dimensionful parameters on the phi-ladder in native units where $c=1$, $\hbar=\phi^{-5}$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the $G_F$ prediction required by the downstream P0-A6 weak neutrino-reference cross-section scorecard, where $\sigma_{\nu,{\rm ref}} = G_F^2 E_{\rm ref}^2 \times$ (GeV$^{-2}\to$ cm$^2$). It therefore closes the P1-C01 slot that feeds every weak-interaction rate calculation in the Recognition framework.

scope and limits

Does not derive the Fermi constant from the J-cost functional equation.
Does not perform unit conversion to laboratory units.
Does not address running or higher-order corrections.
Does not connect $G_F$ to the fine-structure constant band.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.ElectroweakVEVStructure module_import
IndisputableMonolith.Numerics.Interval.W8Bounds module_import

declarations in this module (11)

def row_fermi_pred L50
def row_fermi_codata L54
theorem row_fermi_pred_eq L56
theorem sqrt2_pos L59
theorem fermi_den_pos L61
theorem row_fermi_pred_lower L65
theorem row_fermi_pred_upper L80
theorem row_fermi_pred_bracket L94
theorem row_fermi_codata_in_bracket L98
structure FermiConstantScoreCardCert L103
theorem fermiConstantScoreCardCert_holds L110