sin_cp_angle_nonzero
plain-language theorem explainer
The sine of the RS-derived CP phase is nonzero, so the structural Jarlskog factor cannot vanish. Anyone building the Jarlskog certificate or arguing CP violation from cube geometry will cite this. The proof identifies the CP angle with π/2 from the Berry-phase generators and uses sin(π/2) = 1.
Claim. Let $\delta_{\mathrm{CP}}$ be the CP phase equal to the difference of Berry phases per cycle on the two chirality generators. Then $\sin(\delta_{\mathrm{CP}}) \neq 0$. In the RS derivation one has $\delta_{\mathrm{CP}} = \pi/2$, so $\sin(\delta_{\mathrm{CP}}) = 1$.
background
The Jarlskog invariant $J_{\mathrm{CP}}$ is the unique rephasing-invariant measure of CP violation in the quark sector. In the Wolfenstein parametrization it factors as $J \approx A^2 \lambda^6 \eta \approx A^2 \lambda^6 \sin\delta$. This module builds that structural form from RS inputs: torsion gaps, flip-count asymmetry, and a Berry-phase CP angle.
The eight-tick phases are $k\pi/4$ for $k = 0,\ldots,7$. The CP angle is the raw phase difference between Berry phases per cycle on the two chirality generators; the module records the generator counts as $[4,2,2]\times(\pi/4)$, which collapses to $\pi/2$. The sine of that angle is the factor that decides whether $J$ can be nonzero.
Upstream CKM-from-cube and CP-phase modules supply $\lambda$ (from torsion gap and flip ratio) and $A = 6/11$ (torsion ratio). The present lemma isolates the remaining trigonometric nonvanishing.
proof idea
Tactic proof in two blocks. First, identify the CP angle with $\pi/2$: unfold the angle definition to the raw CP phase, rewrite by the two Berry-generator lemmas (counts $4$ and $2$ times $\pi/4$), and close with ring, recovering $4\cdot(\pi/4) - 2\cdot(\pi/4) = \pi/2$. Second, rewrite the goal under that equality, apply $\sin(\pi/2) = 1$, and finish by norm_num to get $1 \neq 0$.
why it matters
Without $\sin\delta \neq 0$, the structural product $A^2\lambda^6\sin\delta$ collapses and the Jarlskog certificate cannot assert CP violation. Downstream, jarlskogCert wires this lemma in as the sin_cp_nonzero field alongside positivity, smallness, and existence of CP violation.
In the RS chain the result is the trigonometric half of maximal per-cycle CP violation: $\delta = \pi/2$ from the eight-tick Berry difference, so $\sin\delta = 1$. That sits on the T7 eight-tick octave (phases $k\pi/4$) and on the chirality/flip asymmetry already fixed in the CKM-from-cube layer. The module then multiplies by $A = 6/11$ and $\lambda \sim \varphi^{-3}$ to get the hierarchical size of $J$.
The doc-comment is explicit that the laboratory CKM phase may still involve modular arithmetic on the Berry phase; the structural fact needed for $J \neq 0$ is only nonvanishing sine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.