pith. machine review for the scientific record. sign in
def definition def or abbrev high

crossSectionRatio

show as:
view Lean formalization →

RS cosmology sets the dark-matter to neutrino cross-section ratio exactly to the J-cost of the golden ratio. Experimentalists bounding direct-detection rates for the 1.79 GeV candidate cite the quantity when comparing against neutrino backgrounds. The definition is a direct abbreviation that evaluates Cost.Jcost at phi.

claimThe dark-matter to neutrino cross-section ratio equals $J(φ)$, where $J(x) = (x + x^{-1})/2 - 1$.

background

The module records the structural bound on the RS dark-matter prediction, which identifies the candidate at the consciousness-sector boundary of the Higgs vacuum with mass $m_{DM} = m_W/45$. The cross-section ratio $r = σ_{DM}/σ_ν$ is required to equal the canonical golden-section J-cost quantum and to lie in the interval (0.11, 0.13). J-cost is the recognition-cost function drawn from the Cost abbreviation in RSNative.Core; it satisfies the Recognition Composition Law and is evaluated at the self-similar fixed point φ forced by the unified forcing chain.

proof idea

One-line definition that applies Cost.Jcost to phi.

why it matters in Recognition Science

The definition supplies the central quantity used by crossSectionRatio_pos and crossSectionRatio_band to build the DarkMatterCrossSectionCert structure. It realizes T5 J-uniqueness by fixing the observable ratio at the golden-section value, linking the eight-tick octave to cosmology. The module documentation states that exclusion below the band would falsify the identification.

scope and limits

formal statement (Lean)

  31def crossSectionRatio : ℝ := Cost.Jcost phi

proof body

Definition body.

  32
  33/-- The cross-section ratio is strictly positive. -/

used by (3)

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

depends on (5)

Lean names referenced from this declaration's body.