Pith. sign in
module module high

IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard

show as:
view Lean formalization →

This module assembles reference neutrino energy, unit conversions, and weak-channel cross sections for neutrinos and dark matter. It supports Recognition Science phenomenology by normalizing dark-matter predictions to the neutrino reference channel. The module is purely definitional, importing the Fermi constant identity and the J(phi) ratio band without internal theorems.

claim$E_{\rm ref} = 1\,{\rm GeV}$, $\sigma_\nu^{\rm weak\,ref}$ in cm$^2$, $\sigma_{\rm DM}^{\rm weak\,ref} = \sigma_\nu^{\rm weak\,ref} \times J(\phi)$ with $J(\phi) = \phi - 3/2$, plus conversion factor gev2_to_cm2 and band rows.

background

The module sits in the Physics domain and imports FermiConstantScoreCard (Phase 1 row P1-C01, natural-unit electroweak identity) together with DarkMatterCrossSectionBandScoreCard (P0-A6 row, dark-matter to neutrino cross-section ratio given by the recognition quantum $J(\phi) = \phi - 3/2$). It defines the reference energy $E_{\rm ref,GeV}$, the conversion gev2_to_cm2, the reference neutrino cross section $\sigma_\nu^{\rm weak,ref,cm2}$, the corresponding dark-matter value $\sigma_{\rm DM}^{\rm weak,ref,cm2}$, and the two band-row definitions that embed the golden-section ratio.

These objects supply concrete numerical anchors for weak-channel normalization inside the Recognition Science framework, where constants are expressed in native units with $c=1$, $\hbar=\phi^{-5}$, and the phi-ladder mass formula.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete reference values required by the P0-A6 dark-matter cross-section band and the P1-C01 electroweak slice. It therefore feeds any downstream scorecard or phenomenology that compares predicted weak-channel dark-matter rates against neutrino normalization, closing the numerical interface between the Recognition Composition Law and observable cross sections.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)