row_jarlskog_pos
plain-language theorem explainer
The theorem asserts that the predicted Jarlskog invariant for PMNS neutrino mixing is strictly positive. Neutrino physicists assembling CP-violation checks in the Recognition Science framework would cite it when completing the PMNS scorecard. The proof is a direct one-line application of the positivity result already established in the mixing derivation module.
Claim. $0 < J$, where $J$ is the predicted Jarlskog invariant given by the product of the edge dual ratio, fine-structure leakage, torsion overlap, and the sine of the CP phase.
background
The PMNS scorecard module re-uses the CKM-geometry Jarlskog construction to quantify CP violation in neutrino mixing angles and the Dirac phase. The quantity jarlskog_pred is defined as the product (edge_dual_ratio) * fine_structure_leakage * torsion_overlap * sin(ckm_cp_phase), which approximates (1/24) * (α/2) * φ^{-3} * sin(π/2) and represents the geometric area of the unitarity triangle forced by cube topology. Upstream, jarlskog_pos proves this quantity is positive by unfolding the definition and verifying that every factor is positive.
proof idea
This is a one-line wrapper that directly invokes the jarlskog_pos theorem from the MixingDerivation module.
why it matters
The result is consumed by pmnsScoreCardCert_holds to build the nonempty certificate that packages the three mixing-angle rows together with the Jarlskog entry. It thereby supports the geometric origin of CP violation across both CKM and PMNS sectors, consistent with the cube-topology forcing and the phi-ladder structure. The module treats the angle matches as partial theorems and flags scheme dependence of sin²θ_W as a named residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.