Pith. sign in
module module high

IndisputableMonolith.Physics.DarkMatterCrossSectionBandScoreCard

show as:
view Lean formalization →

The module defines the native dark matter to neutrino cross-section ratio as sigma_DM over sigma_nu equal to J(phi). Dark matter modelers and Recognition Science scorecard users cite it for P0-A6 normalization bands. It is a definition module that imports Constants and supplies the ratio without internal proofs.

claimThe ratio satisfies $\frac{\sigma_{DM}}{\sigma_\nu} = J(\phi)$, where $J(x) = \frac{x + x^{-1}}{2} - 1$.

background

Recognition Science builds all physics from the J-cost functional equation and the forcing chain T0-T8. The upstream Constants module supplies the RS-native time quantum $\tau_0 = 1$ tick. This module introduces the cross-section ratio in that setting, using the J-uniqueness property at T5 to fix the functional form.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the ratio that feeds the absolute cross-section normalization scorecard (P0-A6-01) and the weak neutrino-reference scorecard. Both downstream modules apply the band $0.11 < \sigma_{DM}/\sigma_\nu < 0.13$ derived from $J(\phi)$. It closes the link from the T5 J-uniqueness step to observable dark-matter predictions.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)