cp_violation_exists
plain-language theorem explainer
The structural Jarlskog invariant is nonzero, so the quark sector carries genuine CP violation. Anyone citing the RS derivation of matter–antimatter asymmetry from the CKM matrix needs this fact. The proof is a one-line application of positivity: anything strictly positive is unequal to zero.
Claim. The RS structural Jarlskog invariant satisfies $J_{\mathrm{struct}} \neq 0$. Equivalently, the rephasing-invariant measure of CP violation built from torsion gaps, flip-count asymmetry, and the Berry CP angle is nonzero in the quark sector.
background
The Jarlskog invariant $J_{\mathrm{CP}}$ is the unique rephasing-invariant measure of CP violation in the three-generation quark sector. In the Standard Model one has $J = \mathrm{Im}(V_{us} V_{cb} V_{ub}^* V_{cs}^*) \approx 3.08 \times 10^{-5}$. In the Wolfenstein form this is $J = A^2 \lambda^6 \eta \approx A^2 \lambda^6 \sin\delta$.
This module builds a structural stand-in $J_{\mathrm{struct}}$ from Recognition Science ingredients already fixed upstream: torsion gap $\Delta\tau_{12}=11$ and flip ratio $4:2$ fix $\lambda$; the torsion ratio $6/11$ fixes $A$; the Berry phase difference on the cube path $[4,2,2]\times(\pi/4)$ forces $\delta=\pi/2$, hence $\sin\delta=1$. The resulting formula is proportional to $(6/11)^2(\varphi^{-3})^6$.
Sibling results already establish $J_{\mathrm{struct}}>0$ (matter preferred) and the smallness hierarchy from $\varphi$-suppression. The present claim only needs the strict inequality against zero.
proof idea
One-line term proof. Apply the standard order fact ne_of_gt to the already-proved sibling jarlskog_positive, which asserts $J_{\mathrm{struct}}>0$. Strict positivity immediately yields $J_{\mathrm{struct}}\neq 0$. No further algebraic expansion of the structural formula is required at this step.
why it matters
This is the module's central existence claim: the CKM sector supplies a nonzero source term for matter–antimatter asymmetry. The module doc frames it as the statement that CP violation is present in the quark sector ($J\neq 0$).
Downstream it is wired into the master certificate jarlskogCert as the field cp_exists, alongside positivity, smallness, and $\sin\delta\neq 0$. That certificate packages the RS prediction that CP violation is maximal per cycle ($\sin\delta=1$) yet numerically tiny because of $\lambda^6\sim\varphi^{-18}$ suppression, not fine-tuning.
In the broader forcing picture the inputs sit on the cube/Gray-code chirality and Berry-phase side of the Standard Model derivation (CKMFromCube, CPPhaseDerivation), not on the T5–T8 J-cost uniqueness chain itself. The result closes the existence half of the Jarlskog story once positivity is in hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.