dmCrossSection_pos
plain-language theorem explainer
The dark matter cross-section ratio is strictly positive. Researchers modeling XENONnT bounds cite this to confirm the Recognition Science prediction remains allowed. The proof applies the general J-cost positivity lemma at the self-similar fixed point phi using its positivity and inequality to one.
Claim. $0 < Jcost(phi)$ where $Jcost(x)$ denotes the J-cost function and $phi > 1$ is the self-similar fixed point.
background
The module formalizes a dark-matter candidate whose mass ratio to the W boson is 1/45, yielding m_DM between 1.77 and 1.79 GeV. The cross-section ratio is identified with the J-cost evaluated at phi. Upstream, the lemma Jcost_pos_of_ne_one establishes that J(x) exceeds zero for every positive x different from unity; the constants module supplies phi_ne_one. This positivity is the first half of the band certificate that keeps the prediction below current direct-detection limits.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one to the argument phi, using the supplied facts that phi is positive and phi differs from one.
why it matters
This theorem provides the positivity component required by darkMatterXENONCert and by the band theorem dmCrossSection_in_band. It forms part of the A6 Cosmology Depth that predicts an observable dark-matter signal still allowed by present data. The construction rests on the J-uniqueness property (T5) and the forcing of phi as self-similar fixed point (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.