row_sigma_ratio_band
plain-language theorem explainer
The theorem proves the RS-native dark-matter to neutrino cross-section ratio lies strictly between 0.11 and 0.13. Direct-detection experimentalists cite this band when comparing exclusion curves to the golden-section prediction after fixing detector thresholds. The proof is a one-line wrapper that unfolds the definition and applies linear arithmetic to the established bounds on the golden ratio.
Claim. $0.11 < J(φ) ∧ J(φ) < 0.13$ where $J(φ) := φ - 3/2$ and $φ$ is the golden ratio satisfying $1.61 < φ < 1.62$.
background
The module establishes the P0-A6 dark-matter cross-section ratio band. The native ratio is defined as sigma_DM_over_sigma_nu_RS := phi - 3/2, which equals the recognition quantum J(phi). Upstream lemmas from Constants supply the tight bounds 1.61 < phi and phi < 1.62 that place the ratio inside (0.11, 0.13). The module documentation states that this file proves only the RS-native ratio band; absolute normalization and detector-efficiency curves remain empirical.
proof idea
The proof unfolds sigma_DM_over_sigma_nu_RS to phi - 3/2. It splits the conjunction via constructor and applies linarith to each inequality using the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo.
why it matters
This supplies the sigma_ratio_band field to darkMatterCrossSectionBandScoreCardCert_holds and is referenced by darkMatterAbsoluteCrossSectionScoreCardCert_holds and the weak-reference scorecard. It realizes the P0-A6 structural band prediction, anchoring the cross-section claim in the phi-ladder and recognition quantum of the framework. The band remains open to falsification by sub-keV detectors under locked normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.