pith. machine review for the scientific record. sign in
theorem proved term proof high

darkMatterWeakReferenceCrossSectionScoreCardCert_holds

show as:
view Lean formalization →

The theorem certifies existence of a scorecard structure for the P0-A6 weak neutrino reference cross-section channel. It supplies the bands 5.2e-38 to 5.4e-38 cm² for sigma_nu_ref and 5.7e-39 to 7.1e-39 cm² for the derived sigma_DM, together with the Fermi bracket and the 0.11-0.13 RS ratio. Dark-matter detection modelers would cite it to fix the normalization scale against which J(phi) predictions are tested. The proof is a single-term construction that packs the four upstream row theorems into the certificate record.

claimThere exists a certificate $C$ such that $5.2e-38 < sigma_{nu,weak ref} < 5.4e-38$ (cm²), $5.7e-39 < sigma_{DM,weak ref} < 7.1e-39$ (cm²), $1.16e-5 < row_{fermi pred} < 1.17e-5$ (GeV^{-2}), and $0.11 < sigma_{DM}/sigma_{nu,RS} < 0.13$, where the neutrino reference follows $G_F^2 E_{ref}^2$ conversion at $E_{ref}=1$ GeV and the ratio band is obtained from the Recognition Science $J(phi)$ scaling.

background

The module treats the weak neutrino reference as the normalization channel for P0-A6 dark-matter cross-section bounds. It defines sigma_nu_weak_ref_cm2 via the product of the Fermi constant squared, the reference energy squared, and the GeV^{-2} to cm² conversion factor. The certificate structure DarkMatterWeakReferenceCrossSectionScoreCardCert packages four concrete interval constraints that together certify the reference band, the derived DM band, the Fermi prediction bracket, and the RS ratio band. Upstream, row_fermi_pred_bracket supplies the Fermi interval while row_sigma_ratio_band derives the 0.11-0.13 ratio interval from the phi bounds via linarith.

proof idea

The proof is a term-mode one-line wrapper. It directly constructs the certificate record by supplying the four sibling theorems: row_weak_ref_cross_section_band for the neutrino interval, row_sigma_DM_weak_ref_band for the DM interval, row_fermi_pred_bracket for the Fermi bracket, and row_sigma_ratio_band for the ratio interval.

why it matters in Recognition Science

The result closes the arithmetic for the P0-A6 scorecard by confirming the weak-reference bands that normalize dark-matter predictions through the J(phi) ratio. It sits inside the Recognition Science forcing chain at the point where the phi-ladder and RCL composition law determine cross-section ratios. The module doc flags the 1 GeV reference energy as a protocol choice whose falsifier is a sub-0.35 keV detector lying outside the derived band.

scope and limits

formal statement (Lean)

  84theorem darkMatterWeakReferenceCrossSectionScoreCardCert_holds :
  85    Nonempty DarkMatterWeakReferenceCrossSectionScoreCardCert :=

proof body

Term-mode proof.

  86  ⟨{ weak_ref_band := row_weak_ref_cross_section_band
  87     sigma_dm_band := row_sigma_DM_weak_ref_band
  88     fermi_bracket := row_fermi_pred_bracket
  89     sigma_ratio_band := row_sigma_ratio_band }⟩
  90
  91end
  92
  93end IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard

depends on (5)

Lean names referenced from this declaration's body.