band_excludes_falsifier
plain-language theorem explainer
The theorem shows that no measured cross section can simultaneously satisfy the predicted band condition 0.11 σ_ν < σ < 0.13 σ_ν and the falsifying exclusion σ < 0.11 σ_ν. Cosmologists referencing the Recognition Science dark-matter candidate would invoke this result to confirm internal consistency of the J-cost bound. The proof is a direct contradiction obtained by chaining the lower band edge with the falsifier via order transitivity and then applying irreflexivity.
Claim. Let σ and σ_ν be real numbers. It is impossible that both 0.11 σ_ν < σ < 0.13 σ_ν and σ < 0.11 σ_ν hold simultaneously.
background
The module records the structural bound on the dark-matter direct-detection cross section that follows from the J-cost of the golden ratio. The ratio r := σ_DM / σ_ν is required to equal J(φ) and therefore to lie in the open interval (0.11, 0.13). IsInPredictedBand asserts that a measured value falls inside this interval while FalsifiesPrediction asserts that an exclusion limit lies strictly below the lower edge.
proof idea
The term proof assumes the conjunction of the two hypotheses. It extracts the strict lower bound from the band predicate and the strict upper bound from the falsifier predicate, applies lt_trans to obtain σ < σ, and closes with lt_irrefl.
why it matters
The result is packaged inside the DarkMatterCrossSectionCert structure together with positivity and band membership. It thereby certifies the RS prediction that the dark-matter cross section equals J(φ) times the neutrino cross section, closing the consistency check for the identification m_DM ≈ 1.79 GeV. The theorem supplies the mutual-exclusion step required by the module's claim that any exclusion below the band would falsify the candidate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.