jarlskogInvariant
plain-language theorem explainer
The declaration supplies the numerical value 3 × 10^{-5} for the Jarlskog invariant that quantifies CP violation from the complex phase η in the CKM matrix. A researcher working on quark mixing in Recognition Science cites this constant to bound the size of CP-violating effects. The definition is a direct assignment of the approximate value tied to the 8-tick asymmetry.
Claim. The Jarlskog invariant is the real number $3 × 10^{-5}$.
background
The CKM matrix module derives the 3×3 unitary quark mixing matrix from φ-quantized angles linked to the 8-tick phase structure. Wolfenstein parametrization expresses the elements via λ, A, ρ, η, with imaginary parts in V_ub and V_td generating the CP-violating phase. The Jarlskog invariant J measures the area of the unitarity triangle and is set to the approximate experimental scale 3 × 10^{-5}.
proof idea
The definition is a one-line wrapper that directly assigns the constant 3e-5.
why it matters
This definition supplies the input constant for the downstream theorem cp_violation_small, which proves the invariant is positive yet below 10^{-4}. It quantifies the small CP-violating phase arising from 8-tick asymmetry in the Recognition Science derivation of the CKM matrix, connecting to the T7 eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.