FalsifiesPrediction
plain-language theorem explainer
FalsifiesPrediction encodes the condition under which an experimental exclusion of dark-matter cross-section below 0.11 times the neutrino cross-section would rule out the RS identification. Cosmologists and direct-detection experimentalists would cite it when assessing null results against the predicted band. The declaration is introduced as a direct real-number inequality with no additional lemmas.
Claim. Let $σ_{excl}$ be an excluded cross-section and $σ_ν$ the neutrino cross-section. The RS prediction is falsified when $σ_{excl} < 0.11 σ_ν$.
background
The module records the structural bound on dark-matter direct-detection cross-section from the Recognition Science J-cost. The RS candidate is identified as the consciousness-sector boundary of the Higgs vacuum at mass $m_{DM} = m_W/45 ≈ 1.79$ GeV with cross-section $σ_{DM} = J(φ) · σ_ν ≈ 0.118 × 10^{-44}$ cm². The ratio equals the golden-section J-cost quantum and lies in the band (0.11, 0.13). Any exclusion below the lower edge falsifies the identification. Upstream results supply the arithmetic band operation on stable states and the empirical program structure, but this declaration itself is the primitive falsifier predicate.
proof idea
The declaration is a definition that directly states the inequality $σ_{excl} < 0.11 σ_ν$. No lemmas are applied; it serves as the base predicate for the mutual-exclusion theorem and the certification structure.
why it matters
This definition supplies the falsifier predicate that enters the DarkMatterCrossSectionCert structure and the band_excludes_falsifier theorem. It operationalizes the module claim that exclusion below the predicted band falsifies the RS dark-matter identification, which rests on J-uniqueness (T5) and the phi-ladder. The parent theorems establish mutual exclusivity between band membership and this falsifier, closing the logical loop for the cosmology prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.