DarkMatterWeakReferenceCrossSectionScoreCardCert
plain-language theorem explainer
The structure certifies the numerical bands for the weak neutrino reference cross-section and the derived dark matter cross-section under the P0-A6 protocol. Physicists normalizing dark matter signals against the neutrino weak channel would cite these intervals when testing Recognition Science predictions. It is introduced as a direct record of four real-number inequalities drawn from the Fermi constant and the J-derived ratio.
Claim. The certificate asserts the bounds $5.2times10^{-38}<sigma_nu^{rm weak}<5.4times10^{-38}$ cm$^2$ on the reference neutrino cross-section, $5.7times10^{-39}<sigma_{rm DM}<7.1times10^{-39}$ cm$^2$ on the dark matter cross-section, $1.16times10^{-5}<G_F^{rm pred}<1.17times10^{-5}$ GeV$^{-2}$ on the Fermi constant prediction, and $0.11<sigma_{rm DM}/sigma_nu<0.13$ on the Recognition Science ratio.
background
In the Recognition Science framework the cross-section ratio is fixed by the J-function as phi minus 3/2. The reference neutrino cross-section is obtained from the predicted Fermi constant 1 over (sqrt(2) times vev_canonical squared), scaled by the reference energy squared and the GeV^{-2} to cm^2 conversion factor. The module P0-A6 defines the weak reference channel at 1 GeV to normalize dark matter predictions against this channel. Upstream row_fermi_pred supplies the Fermi constant value in GeV^{-2} while sigma_DM_over_sigma_nu_RS supplies the ratio phi minus 3/2; the absolute cross-sections follow by direct scaling.
proof idea
This declaration is a structure definition that directly encodes four interval constraints on the reference quantities. No lemmas are applied and no tactics are used; the fields simply record the stated bounds on the neutrino reference, the derived dark matter cross-section, the Fermi prediction, and the ratio.
why it matters
This structure supplies the certified bands for the P0-A6 weak reference scorecard and is witnessed by the downstream theorem darkMatterWeakReferenceCrossSectionScoreCardCert_holds. It closes the numerical verification step that connects the J-function ratio to observable cross-sections at the 10^{-38} cm^2 scale. The bands rest on the Fermi constant prediction and the eight-tick octave fixed point; an open question remains whether the 1 GeV reference energy is the optimal normalization for all detectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.