DarkMatterCrossSectionCert
plain-language theorem explainer
The structure packages positivity of the dark-matter to neutrino cross-section ratio, its membership in the narrow interval (0.11, 0.13), and mutual exclusion between the predicted detection band and any falsifying exclusion. Recognition Science cosmologists cite it to certify internal consistency of the J-cost dark-matter candidate at roughly 1.79 GeV. The definition is a record whose third field imports the already-proved band-exclusion theorem.
Claim. Let $r = J(phi)$. A certificate is the record type asserting $0 < r$, $0.11 < r < 0.13$, and that the predicates ``measurement lies inside the predicted band'' and ``measurement lies below the lower edge of the band'' cannot hold simultaneously for any real pair of cross sections.
background
The module records the structural bound on the dark-matter cross section that follows from the Recognition Science identification of the candidate as the consciousness-sector boundary of the Higgs vacuum. The ratio $r$ is defined as the J-cost of phi and is required to lie inside (0.11, 0.13) while remaining strictly positive. The local theoretical setting is given by the module documentation: the cross section equals $J(phi)$ times the neutrino cross section, and any exclusion below the lower edge would falsify the identification.
proof idea
The declaration is a structure definition that directly records three field assertions. The first two fields are the positivity and band inequalities on the J-cost ratio. The third field is supplied verbatim by the band_excludes_falsifier theorem, which assumes both predicates and derives a contradiction from the transitivity of the strict order on the reals.
why it matters
The certificate is instantiated by the downstream darkMatterCrossSectionCert definition, which closes the dark-matter cross-section bound in the cosmology module. It supports the RS prediction by confirming that the ratio lies inside the required narrow band and cannot be simultaneously consistent and falsifying. The construction touches the J-uniqueness step of the forcing chain and the phi fixed-point relation that places the ratio near 0.118.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.