crossSectionRatio_pos
plain-language theorem explainer
The theorem establishes that the RS-predicted dark-matter cross-section ratio, equal to the J-cost of the golden ratio, is strictly positive. Cosmologists certifying viability of the direct-detection signal for the m_DM ≈ 1.79 GeV candidate would cite this result. The proof is a short tactic script that derives phi ≠ 1 from the bound phi > 1.5 and applies the general J-cost positivity lemma.
Claim. $0 < J(r)$ where $r$ is the RS-predicted dark-matter cross-section ratio, $J$ is the J-cost function, and $r = J(phi)$ with $phi$ the golden ratio.
background
The module records the structural bound on the dark-matter cross-section from Recognition Science. The cross-section ratio is defined as the J-cost of phi, where J-cost satisfies J(x) > 0 for x > 0 and x ≠ 1. The local setting identifies the dark-matter candidate as the consciousness-sector boundary of the Higgs vacuum with predicted ratio in (0.11, 0.13) and states that the cross-section is strictly positive, permitting RS-canonical detection.
proof idea
The proof unfolds crossSectionRatio to Jcost phi. It derives phi ≠ 1 by assuming equality to 1, obtaining a contradiction with phi > 1.5 via lt_irrefl. It then applies Jcost_pos_of_ne_one using Constants.phi_pos and the derived inequality.
why it matters
This theorem supplies the positivity component of the dark-matter cross-section certificate darkMatterCrossSectionCert. It ensures the predicted cross-section remains positive so that RS-canonical detection is permitted. The result closes the structural bound for the dark-matter identification and records that any exclusion at lower cross-section would falsify the prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.