FalsifiesPrediction
The definition encodes the condition under which an experimental upper limit on dark-matter cross-section falsifies the Recognition Science prediction. Direct-detection physicists would cite it when comparing an observed exclusion to the lower edge of the J(φ) band. The declaration is a direct inequality that sets the falsifier predicate without invoking further lemmas.
claimAn experimental upper bound $σ_{excl}$ on the dark-matter cross section falsifies the prediction precisely when $σ_{excl} < 0.11 σ_ν$, where $σ_ν$ is the neutrino reference cross section.
background
In the Recognition Science setting the dark-matter candidate is identified as the consciousness-sector boundary of the Higgs vacuum at mass $m_{DM} ≈ 1.79$ GeV, producing a predicted cross-section ratio $r = σ_{DM}/σ_ν$ equal to the J-cost $J(φ)$ and required to lie inside the interval (0.11, 0.13). The module records the structural bound that any measured exclusion falling strictly below the lower edge of this band constitutes a falsifier. Upstream results supply the stable-state arithmetic (band operation on 0/1 states) and phase-lift bounds used to establish the interval itself.
proof idea
The declaration is a direct definition whose body is the single inequality $σ_{excl} < 0.11 σ_ν$. No lemmas or tactics are applied; the predicate is introduced by this explicit condition.
why it matters in Recognition Science
This definition supplies the falsification criterion required by the dark-matter cross-section certificate. It is invoked by the theorem band_excludes_falsifier, which proves mutual exclusion between the predicted band and the falsifier, and by the structure DarkMatterCrossSectionCert that packages positivity, band membership, and the exclusion property. The construction closes the empirical test for the RS prediction that the ratio equals $J(φ)$ inside (0.11, 0.13), consistent with the phi-ladder and eight-tick octave of the forcing chain.
scope and limits
- Does not derive the numerical threshold 0.11 from the J-functional equation.
- Does not incorporate detector efficiencies or specific experimental data.
- Does not address the upper edge of the predicted band at 0.13.
- Does not specify units or conversion factors between cross sections.
formal statement (Lean)
66def FalsifiesPrediction (sigma_excl : ℝ) (sigma_nu : ℝ) : Prop :=
proof body
Definition body.
67 sigma_excl < 0.11 * sigma_nu
68
69/-- Predicted band and exclusion-falsifier are mutually exclusive in the
70following sense: a measurement σ that simultaneously sits in the
71predicted band and falsifies the prediction is impossible. -/