Physics Dark Matter Cross Section Band Score Card

The predicted band

Dark matter is the unseen mass that holds galaxies together, but physicists only know it exists through gravity. One of the central questions is how often a dark matter particle would collide with ordinary matter. That rate is called its cross section, a measure of interaction probability. Experiments search for these collisions directly, and their results are plotted as exclusion curves: regions of cross section and mass that no detector has yet ruled out.

Within the Recognition Science framework, the ratio of dark matter's cross section to a neutrino reference channel is not a free parameter. The framework models reality as a ledger, a discrete record of recognition events, and derives a forced cost function from it. That cost function yields the golden ratio φ as a fundamental scaling constant. From that constant, the framework derives a predicted ratio: σ_DM / σ_ν = φ − 3/2, which evaluates to approximately 0.1180.

The module proves this value falls strictly inside the band (0.11, 0.13). This is a theorem in the machine-checked library of formal theorems, with zero unproved assumptions. The proof is simple: it uses the known bounds on φ, namely 1.61 < φ < 1.62, to show the ratio is positive and lies within the stated interval. The certificate structure bundles these two facts into a single checkable object.

The claim is explicitly scoped. The framework derives only the ratio band; the absolute normalization of the cross section and the detector efficiency curves remain empirical inputs. The falsifier is concrete: a detector with sufficient sub-keV reach that excludes the band (0.11, 0.13) under the locked normalization would disprove this prediction. This is a hypothesis with a named test, not an established measurement.

What this establishes in plain language is a target for experiment. If dark matter's interaction strength relative to neutrinos falls in this narrow window, it would be a striking confirmation of the framework's forced constants. If not, the framework's specific prediction is wrong, even though the broader mathematical structure could survive. The module turns a philosophical derivation into a testable number.

/-- Native cross-section ratio, `sigma_DM / sigma_nu = J(phi)`. -/
def sigma_DM_over_sigma_nu_RS : ℝ := phi - 3 / 2

theorem row_sigma_ratio_band :
    0.11 < sigma_DM_over_sigma_nu_RS ∧ sigma_DM_over_sigma_nu_RS < 0.13 := by
  unfold sigma_DM_over_sigma_nu_RS
  constructor
  · linarith [phi_gt_onePointSixOne]
  · linarith [phi_lt_onePointSixTwo]

theorem darkMatterCrossSectionBandScoreCardCert_holds :
    Nonempty DarkMatterCrossSectionBandScoreCardCert :=
  ⟨{ sigma_ratio_pos := row_sigma_ratio_pos
     sigma_ratio_band := row_sigma_ratio_band }⟩

theorem row_sigma_ratio_band :
    0.11 < sigma_DM_over_sigma_nu_RS ∧ sigma_DM_over_sigma_nu_RS < 0.13 := by
  unfold sigma_DM_over_sigma_nu_RS
  constructor
  · linarith [phi_gt_onePointSixOne]
  · linarith [phi_lt_onePointSixTwo]

What this page does not claim

This does not claim the framework derives an absolute dark matter cross section, only a ratio to a neutrino reference. This does not claim the band has been measured; it is a prediction with a named falsifier. This does not claim the framework's derivation of φ itself is empirical; that constant is a theorem, but its physical application here is a hypothesis.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/DarkMatterCrossSectionBandScoreCard.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: