cp_small_but_nonzero
plain-language theorem explainer
The structural Jarlskog invariant is strictly positive and strictly less than one. Quark-sector and baryogenesis work cite this as the SM hallmark: CP violation exists but is hierarchically small. Positivity is delegated to an upstream lemma; the upper bound follows by bounding J by A²=(6/11)² after λ⁶≤1 and sin δ≤1.
Claim. The structural Jarlskog invariant satisfies $0 < J_{\mathrm{struct}} < 1$, where $J_{\mathrm{struct}} = A^2 \lambda^6 \sin\delta$ is built from the RS Wolfenstein parameters $A=6/11$, the torsion-gap $\lambda$, and the Berry-phase CP angle $\delta=\pi/2$.
background
The module derives the Jarlskog invariant $J_{\mathrm{CP}}$ from Q₃ cube geometry. In the Wolfenstein form, $J = A^2 \lambda^6 \eta \approx A^2 \lambda^6 \sin\delta$. Phase 2 (CKMFromCube) fixes $\lambda$ from the torsion gap $\Delta\tau_{12}=11$ and flip ratio 4:2, and fixes $A$ as the torsion ratio $6/11$. Phase 3 (CPPhaseDerivation) fixes the CP angle $\delta=\pi/2$ from the Berry phase difference $[4,2,2]\times(\pi/4)$, so $\sin\delta=1$.
The structural prediction is therefore $J \propto (6/11)^2 \lambda^6$. Upstream, A_structural_value states $A=6/11$. Sibling results already give $J>0$ (matter preferred) and the $\lambda$-hierarchy $\lambda^6<1$ from $\varphi$-suppression. The present claim packages positivity with a strict upper bound $J<1$, the SM hallmark that CP violation is present yet small without fine-tuning.
proof idea
Split the conjunction. The left conjunct is exactly the sibling lemma jarlskog_positive.
For the right conjunct, unfold the structural formula $J=A^2\lambda^6\sin\delta$. Rewrite $A^2=(6/11)^2$ via A_structural_value and check $(6/11)^2<1$ by norm_num. Use jarlskog_hierarchy to get $\lambda^6\le 1$, nonnegativity of $\lambda^6$ from $\varphi>0$, and $\sin\delta\le 1$. A short computation shows $\delta=\pi/2$ (Berry generators), hence $\sin\delta=1\ge 0$. Then nlinarith multiplies the bounds to conclude $J\le A^2<1$.
why it matters
This is the module's "small but nonzero" packaging of CP violation: positivity from matter preference, smallness from $\lambda^6$ ($\varphi$-suppression), not parameter tuning. The doc-comment states the SM hallmark explicitly.
Downstream, jarlskogCert records the upper bound as its small field, completing the master certificate alongside positivity, nonzero $\sin\delta$, and existence of CP violation. Cosmology reuses the same bound: eta_B_small divides by $g_*=106.75$ and applies $J<1$ to show the structural baryon asymmetry $\eta_B<1$.
In the broader RS chain this sits after CKM-from-cube and Berry-phase CP derivation; it does not itself invoke T5–T8, but inherits $\varphi$ through the $\lambda$ ladder and the eight-tick geometric origin of the cube torsion gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.