darkMatterAbsoluteCrossSectionScoreCardCert_holds
plain-language theorem explainer
The declaration certifies existence of a scorecard structure for the absolute dark matter cross section under the Recognition Science protocol normalization. Experimental physicists comparing direct detection limits to the predicted band would cite it when assessing sigma_DM against detector thresholds. The proof is a term-mode construction that assembles the certificate from three row theorems establishing positivity, the ratio interval, and the absolute interval.
Claim. There exists a certificate such that the reference neutrino cross section satisfies $0 < sigma_nu_reference_cm2$, the Recognition Science ratio satisfies $0.11 < sigma_DM_over_sigma_nu_RS < 0.13$, and the absolute dark matter cross section satisfies $1.1e-39 < sigma_DM_cm2 < 1.3e-39$ cm$^2$.
background
The module treats P0-A6, the absolute cross-section normalization scorecard. The certificate structure DarkMatterAbsoluteCrossSectionScoreCardCert requires three fields: positivity of sigma_nu_reference_cm2 (the protocol value 1e-38 cm$^2$), the ratio band on sigma_DM_over_sigma_nu_RS, and the derived absolute band on sigma_DM_cm2. The predicted relation is sigma_DM = (sigma_DM/sigma_nu) * sigma_nu_ref with the ratio interval (0.11, 0.13) and target band (1.1e-39, 1.3e-39) cm$^2$ after a sub-0.35 keV efficiency curve is supplied.
proof idea
The proof is a term-mode construction that directly builds the certificate structure. It supplies sigma_nu_ref_pos from row_sigma_nu_reference_pos, sigma_ratio_band from row_sigma_ratio_band, and sigma_absolute_band from row_sigma_DM_cm2_band. The upstream row_sigma_ratio_band uses linarith on the phi bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo; row_sigma_DM_cm2_band applies nlinarith after unfolding the definitions.
why it matters
The theorem completes the certificate for P0-A6, confirming the absolute band follows from the named protocol normalization and the RS ratio band. It supports detector-limit comparisons in direct dark matter searches. The module doc notes the open question of deriving the neutrino reference normalization from RS or a specified channel, which remains untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.