row_sigma_nu_reference_pos
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.