darkMatterCrossSectionCert
plain-language theorem explainer
The declaration assembles a certificate structure asserting that the dark-matter to neutrino cross-section ratio is strictly positive, lies inside the open interval (0.11, 0.13), and cannot simultaneously occupy the predicted band while falsifying the underlying identification. Cosmologists using the Recognition Science framework would cite this certificate when confronting the predicted direct-detection cross-section against experimental upper limits. The definition is assembled by direct substitution of three prior theorems that separately 0.
Claim. The dark-matter cross-section certificate is the structure asserting $0 < r$, $0.11 < r < 0.13$, and that for all real numbers $sigma, sigma_nu$ it is impossible for both IsInPredictedBand$(sigma, sigma_nu)$ and FalsifiesPrediction$(sigma, sigma_nu)$ to hold, where $r$ denotes the ratio of the predicted dark-matter cross-section to the neutrino cross-section.
background
The module records the structural consequences of the Recognition Science dark-matter identification, which places the candidate at the consciousness-sector boundary of the Higgs vacuum with mass $m_{DM} = m_W / 45$ and cross-section $sigma_{DM} = J(phi) cdot sigma_nu$. The cross-section ratio is therefore identified with the J-cost of phi and is required to satisfy three properties: strict positivity, membership in the canonical band (0.11, 0.13), and logical exclusion between band membership and any falsifying measurement. These properties are supplied by the three upstream theorems crossSectionRatio_pos, crossSectionRatio_band, and band_excludes_falsifier.
proof idea
The definition is a one-line wrapper that constructs the DarkMatterCrossSectionCert structure by supplying the three component proofs: crossSectionRatio_pos for the positivity field, crossSectionRatio_band for the interval field, and band_excludes_falsifier for the exclusion field.
why it matters
This certificate supplies the Lean witness that the predicted cross-section ratio satisfies the three structural requirements of the dark-matter identification. It thereby makes the J-cost prediction available for comparison with direct-detection experiments while remaining inside the Recognition Science derivation that all interaction scales descend from the phi-ladder. The construction closes the structural side of the cosmology module and rests on the J-cost definition together with the phi inequalities established in Constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.