DarkMatterCrossSectionBandScoreCardCert
plain-language theorem explainer
Physicists comparing direct-detection exclusion curves to Recognition Science predictions would cite this certificate for the dark-matter to neutrino cross-section ratio. It records that the ratio defined by J(phi) = phi - 3/2 is positive and lies inside the open interval (0.11, 0.13). The declaration is a plain structure whose two fields simply assert the required inequalities on the precomputed ratio value.
Claim. Let $r = J(phi) = phi - 3/2$ denote the native dark-matter to neutrino cross-section ratio. The certificate asserts $0 < r$ together with $0.11 < r < 0.13$.
background
The module treats row P0-A6 of the Recognition Science scorecard, which concerns the structural band for the dark-matter cross-section ratio. The upstream definition supplies the ratio explicitly as sigma_DM_over_sigma_nu_RS := phi - 3/2, described in its doc-comment as the native cross-section ratio sigma_DM / sigma_nu = J(phi). The module doc states that this file proves only the RS-native ratio band; absolute normalization and detector-efficiency curves remain empirical.
proof idea
The declaration is a structure definition whose fields directly encode the positivity and band inequalities on the constant sigma_DM_over_sigma_nu_RS. No lemmas or tactics are invoked; the structure simply packages the two propositions as a record type.
why it matters
The structure is the certificate type whose non-emptiness is witnessed by the downstream theorem darkMatterCrossSectionBandScoreCardCert_holds. It supplies the concrete band (0.11, 0.13) required by the P0-A6 claim in the Recognition Science framework. The module doc identifies the falsifier as a sub-keV detector that excludes the band under locked normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.