row_sigma_nu_reference_pos
The theorem establishes positivity of the neutrino reference cross-section normalization at 10^{-38} cm². Dark matter detection groups referencing the P0-A6 scorecard cite it to anchor absolute cross-section band calculations. The proof is a one-line term wrapper that unfolds the constant definition and applies numerical normalization.
claim$0 < 10^{-38} = 10^{-38}$ where the left-hand side is the protocol normalization for the neutrino-reference channel in cm² units.
background
The module defines sigma_nu_reference_cm2 explicitly as the protocol normalization for the neutrino-reference channel, set to the literal value 1e-38 in cm². This constant enters the predicted formula sigma_DM = (sigma_DM/sigma_nu) * sigma_nu_ref with the ratio band constrained between 0.11 and 0.13. The local setting is the P0-A6 absolute cross-section normalization scorecard, whose target band is (1.1e-39, 1.3e-39) cm² once a sub-0.35 keV efficiency curve is supplied.
proof idea
The proof unfolds the definition of sigma_nu_reference_cm2 to expose the constant 1e-38 and then applies the norm_num tactic to discharge the strict inequality.
why it matters in Recognition Science
It supplies the positivity witness required by darkMatterAbsoluteCrossSectionScoreCardCert_holds to build the scorecard certificate. The result completes the P0-A6 row in the Recognition Science physics module, where the adopted normalization anchors absolute dark-matter cross-section predictions. The module status remains PARTIAL_THEOREM because deriving the reference value from the RS forcing chain or RCL is still open.
scope and limits
- Does not derive the numerical normalization from Recognition Science primitives or the forcing chain.
- Does not incorporate detector efficiency curves at or below 0.35 keV.
- Does not compute or constrain the dark-matter to neutrino ratio band.
- Does not construct the full scorecard certificate.
Lean usage
theorem cert_holds : Nonempty DarkMatterAbsoluteCrossSectionScoreCardCert := ⟨{ sigma_nu_ref_pos := row_sigma_nu_reference_pos, sigma_ratio_band := row_sigma_ratio_band, sigma_absolute_band := row_sigma_DM_cm2_band }⟩formal statement (Lean)
40theorem row_sigma_nu_reference_pos : 0 < sigma_nu_reference_cm2 := by
proof body
Term-mode proof.
41 unfold sigma_nu_reference_cm2
42 norm_num
43