darkMatterWeakReferenceCrossSectionScoreCardCert_holds
plain-language theorem explainer
Physicists normalizing dark matter direct detection limits against the neutrino weak reference channel would cite this result to confirm the Recognition Science cross-section bands for the 1 GeV normalization. The declaration shows that the four component inequalities assemble into a non-empty certificate structure. Its proof is a direct term construction that packages the upstream row theorems for the weak reference band, DM band, Fermi bracket, and RS ratio without further steps.
Claim. The certificate structure is inhabited: there exist values satisfying $5.2e-38 < sigma_nu_weak_ref_cm2 < 5.4e-38$, $5.7e-39 < sigma_DM_weak_ref_cm2 < 7.1e-39$, $(1.16e-5 : R) < row_fermi_pred < (1.17e-5 : R)$, and $0.11 < sigma_DM_over_sigma_nu_RS < 0.13$.
background
The module sets the P0-A6 weak neutrino-reference cross-section scorecard. It adopts the reference formula sigma_nu_ref = G_F^2 * E_ref^2 * (GeV^-2 to cm^2) at E_ref = 1 GeV with conversion 0.3894e-27, yielding the target interval 5.2e-38 < sigma_nu_ref < 5.4e-38 cm^2 and the derived DM interval 5.7e-39 < sigma_DM < 7.1e-39 cm^2 from the J(phi) ratio. The certificate structure requires exactly these four bands together with the Fermi bracket and the RS ratio band. Upstream, row_fermi_pred_bracket supplies the Fermi interval, row_sigma_ratio_band establishes the 0.11-0.13 ratio via phi bounds, row_weak_ref_cross_section_band proves the neutrino reference interval from the Fermi bracket and conversion factors, and row_sigma_DM_weak_ref_band derives the DM interval from the reference band and ratio.
proof idea
The proof is a term that constructs the certificate record by directly supplying the four upstream theorems: row_weak_ref_cross_section_band for the weak reference band, row_sigma_DM_weak_ref_band for the DM band, row_fermi_pred_bracket for the Fermi bracket, and row_sigma_ratio_band for the ratio band.
why it matters
This theorem certifies the P0-A6 weak reference normalization inside the Recognition Science framework, closing the arithmetic chain from the J(phi) ratio to observable cross-section bands. It supports the dark matter cross-section predictions that feed into the phi-ladder mass formulas and the eight-tick octave structure. The module doc notes that the 1 GeV reference choice remains a protocol normalization rather than a derived result; no downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.