E_ref_GeV
plain-language theorem explainer
The definition assigns the reference neutrino energy to exactly 1 GeV for normalizing the weak interaction cross-section channel. Modelers of dark-matter detection via neutrino reference bands cite this constant when evaluating the P0-A6 scorecard predictions. It enters as a direct numerical assignment with no further reduction steps.
Claim. The reference neutrino energy for weak-channel normalization is defined by $E_0 = 1$ GeV.
background
The module supplies the P0-A6 weak neutrino-reference cross-section scorecard. It fixes the reference energy at 1 GeV so that the predicted weak cross section reads $G_F^2 E_0^2$ times the conversion factor 0.3894e-27 cm^2/GeV^{-2}. This produces the numerical interval 5.2e-38 < sigma_nu_ref < 5.4e-38 cm^2 and, via the J(phi) factor, the derived dark-matter band 5.7e-39 < sigma_DM < 7.1e-39 cm^2. The module documentation states that the arithmetic follows from the Fermi scorecard while the 1 GeV choice remains a protocol normalization.
proof idea
The declaration is a direct constant definition that assigns the literal value 1. No lemmas or tactics are invoked.
why it matters
The constant is unfolded inside sigma_nu_weak_ref_cm2 and row_weak_ref_cross_section_band, the latter proving the concrete numerical band for the weak reference. It supplies the normalization step required by the P0-A6 scorecard in the Recognition Science cross-section derivation. The module notes that the 1 GeV choice is a protocol hypothesis that links the Fermi constant to the J(phi)-based dark-matter prediction; altering the reference energy would require replacement of this row.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.