Pith. sign in
module module high

IndisputableMonolith.StandardModel.JarlskogInvariant

show as:
view Lean formalization →

Module packaging the Jarlskog invariant of quark mixing from RS geometry: the CP phase is the Berry-phase difference on the directed Gray-code cycle, fixed at δ = π/2. It proves structural positivity and hierarchy of J_CP and that CP violation is small but nonzero. Cosmology cites it for the sign of baryon asymmetry. Arguments reduce to the cube CKM construction and the Gray-code chirality lemmas.

claimThe CP phase is $\delta = \gamma(\mathrm{gen}_1) - \gamma(\mathrm{gen}_2) = \pi/2$ from Berry phases on the directed 8-tick Gray-code cycle. The Jarlskog invariant $J_{\mathrm{CP}}$ built from the RS CKM data is structurally positive, obeys the expected hierarchy, and yields $\sin\delta \neq 0$, so CP violation exists and is small but nonzero.

background

Recognition Science places quark mixing on the 3-cube $Q_3$. The CKM module builds the mixing matrix from generation torsion ${0,11,17}$ and the Gray-code edge pattern $[4,2,2]$. Independently, Gray-code chirality shows that the canonical directed 3-bit cycle on $Q_3$ distinguishes orientation of face boundaries; that geometric handedness is the RS origin of CP violation.

The CP-phase module accumulates a Berry phase for each generation eigenstate transported around the eight-tick cycle. The present module takes the difference of those phases as the CKM CP angle: $\delta = \gamma(\mathrm{gen}_1)-\gamma(\mathrm{gen}_2)=4(\pi/4)-2(\pi/4)=\pi/2$. The Jarlskog invariant is the unique (up to convention) rephasing-invariant measure of CP violation in the three-generation CKM matrix; here it is evaluated on the RS structural CKM data rather than on fitted angles.

Constants supply the RS tick $\tau_0$ used to normalize the cycle. Downstream cosmology only needs the sign and nonvanishing of $J_{\mathrm{CP}}$, not a precision fit to the experimental Jarlskog number.

proof idea

The module is a short certificate layer, not a long derivation. It defines cpAngle as the Berry-phase difference already computed in CPPhaseDerivation, obtaining $\delta=\pi/2$. Nonvanishing of $\sin\delta$ is immediate from that value.

Structural Jarlskog quantities are assembled from the CKM-from-cube matrix entries and the fixed phase. Positivity and hierarchy lemmas are algebraic consequences of the Gray-code chirality orientation and the generation-torsion magnitudes. Existence of CP violation and the "small but nonzero" statement package those facts into named theorems and a JarlskogCert bundle for importers.

No independent geometric work happens here: every nontrivial step cites CKMFromCube or GrayCodeChirality (via the phase module).

why it matters in Recognition Science

Sakharov's second condition demands C and CP violation for baryogenesis. This module supplies the RS-native, structurally positive Jarlskog invariant that witnesses that condition.

BaryonAsymmetryDerivation states explicitly that the theorem content $\eta_B>0$ follows from $J_{\mathrm{CP}}>0$ (Jarlskog from Gray-code chirality) plus the Sakharov conditions; the numerical scaffold for $\eta_B$ is separate. BaryogenesisStaging and SakharovFromLedger import the same nonvanishing CP fact so the ledger lane cannot fake a missing mechanism.

In the forcing picture the result sits downstream of T7 (eight-tick octave) and the $D=3$ cube geometry: the directed Gray cycle on $Q_3$ is chiral, the Berry phase difference is $\pi/2$, and $J_{\mathrm{CP}}$ cannot vanish. That closes the CP-violation input to the matter-antimatter sign without fitting $\delta$ by hand.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (9)