IsInPredictedBand
Defines the arithmetic condition for a measured dark matter cross section to fall inside the interval predicted by the J-cost of the golden ratio. Cosmologists would cite this predicate when testing direct-detection data against the Recognition Science forecast of approximately 0.118 times the neutrino cross section. It is realized as a direct conjunction of two strict inequalities.
claimA measured cross-section $σ_{meas}$ lies in the predicted band if $0.11 σ_ν < σ_{meas} < 0.13 σ_ν$, where $σ_ν$ denotes the reference neutrino cross-section.
background
In the Recognition Science treatment of dark matter the candidate is identified as the consciousness-sector boundary of the Higgs vacuum at mass $m_{DM} = m_W/45 ≈ 1.79$ GeV. Its direct-detection cross section is $σ_{DM} = J(φ) · σ_ν ≈ 0.118 × 10^{-44}$ cm², with the ratio fixed by the J-cost function $J(x) = (x + x^{-1})/2 - 1$. The module records the structural bound that this ratio must occupy the open interval (0.11, 0.13).
proof idea
The definition directly implements the two-sided inequality without invoking lemmas or tactics; it is a one-line abbreviation of the band condition.
why it matters in Recognition Science
The predicate supplies the positive consistency clause for the certificate structure DarkMatterCrossSectionCert and is invoked in the mutual-exclusion theorem band_excludes_falsifier. It thereby anchors the dark-matter cross-section prediction to the J-uniqueness step (T5) of the forcing chain and closes one consistency check in the cosmology module.
scope and limits
- Does not derive the band limits from the forcing chain.
- Does not incorporate experimental resolution or background subtraction.
- Does not assert that any real measurement satisfies the predicate.
- Does not extend to indirect detection channels or relic density constraints.
formal statement (Lean)
62def IsInPredictedBand (sigma_meas : ℝ) (sigma_nu : ℝ) : Prop :=
proof body
Definition body.
63 0.11 * sigma_nu < sigma_meas ∧ sigma_meas < 0.13 * sigma_nu
64
65/-- Exclusion below the predicted band of cross-section is a falsifier. -/