module module high

`IndisputableMonolith.Constants.FermiConstantScoreCard`

The module supplies the P1-C01 Fermi constant prediction scorecard in GeV^{-2} natural units. Researchers comparing RS electroweak constants to data or building dark-matter cross-section scorecards would cite it. The module assembles predicted and codata rows together with positivity and bracket lemmas drawn from the electroweak VEV structure and eight-tick weight bounds.

claimFermi constant prediction scorecard: $G_F$ (GeV$^{-2}$) with predicted row, codata row, and certified bracket.

background

The module sits in the constants domain and imports the ElectroweakVEVStructure module, which formalizes the RS structural framework for the electroweak VEV $v ≈ 246$ GeV (C-020). It also imports W8Bounds, whose doc-comment states that the gap weight $w_8$ from the eight-tick octave is the closed-form expression $(348 + 210√2 - (204 + 130√2)φ)/7 ≈ 2.490569$. Sibling definitions supply rows for the predicted Fermi constant, codata values, positivity facts, and a certificate that the prediction lies inside the codata interval.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the P1-C01 entry imported by the DarkMatterWeakReferenceCrossSectionScoreCard module (P0-A6), whose doc-comment gives the reference cross-section formula $σ_{ν ref} = G_F^2 E_{ref}^2$ (GeV$^{-2}$ to cm$^2$). It therefore completes the Fermi-constant link required for the weak-reference channel in the Recognition Science constants registry.

scope and limits

Does not derive $G_F$ from the full T0-T8 forcing chain.
Does not include experimental uncertainties beyond the codata row.
Does not perform unit conversions outside natural units.
Does not relate $G_F$ to the fine-structure constant or Newtonian $G$.

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