darkMatterCrossSectionBandScoreCardCert_holds
plain-language theorem explainer
The theorem certifies that a structure witnessing the dark-matter to neutrino cross-section ratio band is inhabited. Direct-detection physicists would cite it when testing exclusion curves against the RS-native interval (0.11, 0.13). The proof is a one-line term that assembles the positivity and band theorems into the required certificate structure.
Claim. The certificate structure for the dark-matter cross-section ratio band is nonempty: there exists a value of the RS-native ratio satisfying $0 < r$ and $0.11 < r < 0.13$, where $r = J(phi) = phi - 3/2$.
background
In Recognition Science the dark-matter cross-section ratio to the neutrino reference channel is the J-cost evaluated at the golden ratio: $r = J(phi) = phi - 3/2$. Module P0-A6 supplies the structural band for this ratio so that direct-detection exclusion curves can be compared after detector thresholds are fixed. The certificate structure requires both strict positivity of the ratio and membership in the open interval (0.11, 0.13). Upstream lemmas establish positivity by comparison with $phi > 1.618$ and the band bounds by comparison with $phi < 1.62$.
proof idea
The proof is a term-mode construction that directly instantiates the certificate structure. It supplies the field sigma_ratio_pos with the theorem row_sigma_ratio_pos and the field sigma_ratio_band with the theorem row_sigma_ratio_band.
why it matters
This theorem completes the native certification of the P0-A6 dark-matter cross-section ratio band. It supplies the concrete interval predicted by J-uniqueness (T5) for comparison with direct-detection data. Absolute normalization and detector-efficiency curves remain empirical; the result therefore closes the structural part of the claim while leaving the full experimental protocol open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.