row_weak_ref_cross_section_band
plain-language theorem explainer
The theorem pins the weak neutrino reference cross section to the open interval (5.2e-38, 5.4e-38) cm². Dark matter experimenters constructing P0-A6 normalization bands cite this bound when converting the Fermi constant prediction into an absolute weak-channel reference. The proof reduces the claim to the known Fermi bracket by unfolding the quadratic expression and closing both inequalities with nlinarith after a positivity step.
Claim. $5.2×10^{-38} < σ_ν^{weak,ref} < 5.4×10^{-38}$ cm², where $σ_ν^{weak,ref} := G_F^2 · (1 GeV)^2 · 0.3894×10^{-27}$ cm²/GeV² and $G_F$ is the predicted Fermi constant in GeV^{-2}.
background
Module P0-A6 supplies the weak neutrino reference channel used to normalize dark matter cross-section ratios. The reference energy is fixed at 1 GeV and the unit conversion is defined as 0.3894e-27 cm² per GeV^{-2}. The Fermi constant prediction equals 1/(√2 · vev_canonical²) and its bracket theorem supplies the numerical interval (1.16e-5, 1.17e-5) in GeV^{-2}. The reference cross section is then obtained by squaring the Fermi value, multiplying by the reference energy squared, and scaling by the conversion factor.
proof idea
The proof unfolds sigma_nu_weak_ref_cm2, E_ref_GeV and gev2_to_cm2 to expose the quadratic dependence on row_fermi_pred. It obtains the Fermi bracket via row_fermi_pred_bracket, proves positivity of row_fermi_pred by linarith, and applies nlinarith to both sides of the target inequality.
why it matters
The bound is required by darkMatterWeakReferenceCrossSectionScoreCardCert_holds and by row_sigma_DM_weak_ref_band, which derives the corresponding dark matter interval (5.7e-39, 7.1e-39) cm². It implements the P0-A6 protocol step that normalizes the J(phi)-derived dark matter cross section against the standard weak interaction strength. The 1 GeV reference choice remains a protocol convention whose falsifier is a detector measurement lying outside the derived band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.