row_jarlskog
plain-language theorem explainer
The declaration certifies that the RS geometric prediction for the Jarlskog invariant lies within 20% of the observed central value 3.08e-5. Neutrino physicists auditing CP violation in the lepton sector would cite the result when checking the PMNS scorecard against PDG or NuFIT data. The proof is a direct one-line wrapper that invokes the upstream jarlskog_match theorem.
Claim. Let $J$ denote the Jarlskog invariant constructed geometrically as the product of the edge dual ratio, fine-structure leakage, torsion overlap, and the sine of the CP phase. Then $|J - 3.08times 10^{-5}| < 0.6times 10^{-5}$.
background
The PMNSScoreCard module assembles rows that certify RS predictions for the full PMNS mixing matrix against PDG/NuFIT centers, including the Jarlskog invariant as a measure of CP violation. The Jarlskog invariant $J_{CP}$ is the geometric area of the unitarity triangle, forced by cube topology and fine-structure leakage, with the explicit form $J = s_{12}s_{23}s_{13}c_{12}c_{23}c_{13}sin delta$ and the RS approximation $J approx (1/24)cdot (alpha/2)cdot phi^{-3}cdot sin(pi/2)$. Upstream results in MixingDerivation supply both the definition of the predicted value and the match theorem that requires transcendental bounds on alpha and phi.
proof idea
The proof is a one-line wrapper that applies the jarlskog_match theorem from MixingDerivation. That upstream theorem establishes the numerical bound by direct comparison of the geometric approximation (yielding approximately 3.03e-5) to the target 3.08e-5, keeping Constants.alpha opaque and reducing only the sine term to unity.
why it matters
This row supplies the Jarlskog entry inside the PMNSScoreCardCert record that is assembled by pmnsScoreCardCert_holds, completing the packaged scorecard for PMNS mixing. It realizes the geometric origin of CP violation within the Recognition framework, tying the cube topology and fine-structure leakage to the observed J_CP value inside the alpha band. The module doc notes that any NuFIT/PDG update moving a central value outside the certified error without compensating changes to RS inputs (alpha, phi bounds) falsifies the match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.