DarkMatterAbsoluteCrossSectionScoreCardCert
plain-language theorem explainer
The DarkMatterAbsoluteCrossSectionScoreCardCert structure packages the positivity of the neutrino reference cross section together with the RS-predicted ratio band and the resulting absolute dark-matter cross-section band in cm^2. Direct-detection experimentalists would cite this certificate when mapping RS predictions onto detector sensitivity limits. It is realized as a structure definition that simply collects the three numerical inequalities supplied by the upstream ratio and normalization definitions.
Claim. Let $0 < 10^{-38}$ denote the neutrino reference cross section in cm$^2$, let $0.11 < r < 0.13$ be the RS ratio $r = sigma_DM_over_sigma_nu_RS$, and let $sigma_DM = r times 10^{-38}$. The certificate asserts the three conditions $0 < 10^{-38}$, $0.11 < r < 0.13$, and $1.1 times 10^{-39} < sigma_DM < 1.3 times 10^{-39}$.
background
This declaration belongs to the P0-A6 scorecard for absolute cross-section normalization. The local setting is a protocol normalization in which the dark-matter cross section is obtained by multiplying the RS-native ratio by the reference value $sigma_nu_reference_cm2 = 10^{-38}$ cm$^2$, yielding the absolute band after multiplication. The upstream definitions supply $sigma_nu_reference_cm2 := 10^{-38}$, $sigma_DM_over_sigma_nu_RS := phi - 3/2$, and $sigma_DM_cm2 := sigma_DM_over_sigma_nu_RS times sigma_nu_reference_cm2$. The module documentation states that detector-limit comparisons should use the derived band only after a sub-0.35 keV efficiency curve is supplied.
proof idea
The structure is introduced by a direct definition that enumerates the three required field propositions. No lemmas are applied; the fields are populated by the concrete numerical values and inequalities already established in the sibling definitions sigma_nu_reference_cm2, sigma_DM_over_sigma_nu_RS, and sigma_DM_cm2.
why it matters
This certificate supplies the concrete data structure consumed by the theorem darkMatterAbsoluteCrossSectionScoreCardCert_holds, which constructs a witness showing the structure is inhabited. It realizes the P0-A6 row of the absolute cross-section scorecard, closing the numerical band under the current protocol normalization. The module documentation notes that deriving the reference normalization from RS primitives or a specified neutrino channel remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.