row_sigma_ratio_pos
plain-language theorem explainer
The theorem proves that the RS-native dark-matter to neutrino cross-section ratio is strictly positive. Direct-detection experimentalists would cite it when anchoring exclusion curves to the predicted structural band. The proof is a one-line term wrapper that unfolds the ratio definition and applies linarith to the upstream bound phi > 1.61.
Claim. $0 < J(phi)$ where $J(phi) := phi - 3/2$ and $phi$ is the golden ratio satisfying the Recognition Composition Law.
background
The module P0-A6 treats the dark-matter cross-section ratio as the recognition quantum J(phi) = phi - 3/2. This quantity supplies the structural band against which direct-detection exclusion curves are compared once detector thresholds and efficiencies are fixed. The upstream lemma phi_gt_onePointSixOne states that phi > 1.61 and is invoked directly to guarantee positivity of the ratio.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition sigma_DM_over_sigma_nu_RS := phi - 3/2 and invokes linarith on the hypothesis supplied by phi_gt_onePointSixOne.
why it matters
The result supplies the positivity field of DarkMatterCrossSectionBandScoreCardCert_holds, which certifies the P0-A6 structural band. It closes the positivity check required by the Recognition Science prediction that the ratio lies inside (0.11, 0.13). Absolute normalization and detector-efficiency curves remain empirical open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.