jarlskog
plain-language theorem explainer
The jarlskog definition supplies the predicted Jarlskog invariant for CKM phenomenology. Researchers comparing geometric CP-violation measures to the observed value near 3.08e-5 would cite this alias when checking quark-mixing predictions. It is realized as a direct one-line assignment to the upstream jarlskog_pred computation derived from rung differences on the phi-ladder.
Claim. Define the Jarlskog invariant by $J := J_{pred}$, where $J_{pred}$ is the geometric area of the unitarity triangle given by $J_{pred} = s_{12}s_{23}s_{13}c_{12}c_{23}c_{13}sinδ$ and approximated as $J_{pred} ≈ (1/24)·(α/2)·φ^{-3}·sin(π/2)$.
background
The CKM module derives mixing angles from rung differences between up and down quark generations (τ_g = 0, 11, 17) on the phi-ladder, producing θ_ij ~ φ^{-Δτ/2} and a CP phase from residue asymmetry. The Jarlskog invariant J = Im(V_ud V_cb V_ub^* V_cd^*) appears as a forced dimensionless output with no free parameters fitted to data. The local setting is stated in the module documentation as CKM Matrix and Jarlskog Invariant from φ-Ladder, grounded in geometric proofs from MixingDerivation.
proof idea
This declaration is a one-line wrapper that directly aliases jarlskog_pred from the MixingDerivation module.
why it matters
The definition supplies the Jarlskog value to the CKMPhenomenology structure and the jarlskog_summary lemma, which in turn feed PMNSScoreCardCert and pmnsScoreCardCert_holds for scorecard validation against experiment. It completes the geometric derivation of CP violation in the CKM sector as described in the module documentation, linking rung assignments on the phi-ladder to the forced CP phase. The construction sits inside the Recognition Science forcing chain after T5 J-uniqueness and T6 phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.