dmCrossSectionRatio
plain-language theorem explainer
The declaration defines the dark matter cross-section ratio as the J-cost evaluated at the golden ratio φ. Cosmologists testing Recognition Science predictions against XENON detector bounds would cite this to anchor the expected interaction strength. It is realized as a direct noncomputable definition with no further reduction.
Claim. The dark matter cross-section ratio is defined as $J(φ)$, where $J$ is the J-cost function and $φ$ is the golden ratio.
background
The module formalizes dark matter predictions in Recognition Science cosmology, stating that the mass ratio m_DM / m_W equals 1/45 and therefore m_DM lies in (1.77, 1.79) GeV. The cross-section ratio is fixed at J(φ) to occupy the interval (0.11, 0.13), which lies above the current XENONnT exclusion at 1.78 GeV. The setting draws on the J-cost from the Cost module together with the constant φ, while upstream dependencies supply collision-free empirical program properties and algebraic ledger consistency.
proof idea
This is a one-line definition that directly assigns the cross-section ratio to Jcost applied to phi.
why it matters
The definition supplies the cross-section ratio required by DarkMatterXENONCert and the supporting theorems dmCrossSection_pos and dmCrossSection_in_band, which together certify that the RS prediction remains unexcluded. It completes the A6 Cosmology Depth by providing the concrete J(φ) band anchor, connecting to the phi-ladder and the T5–T8 forcing chain. No open scaffolding questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.