Pith. sign in
module module high

IndisputableMonolith.StandardModel.CPPhaseDerivation

show as:
view Lean formalization →

Derives the quark-sector CP-violating phase from Berry phases accumulated along the canonical Gray-code transport path on the three-cube. Generation-dependent phases arise from face windings and the chiral eight-tick cycle; their imbalance yields a nonzero raw CP phase. Cited by anyone extracting Jarlskog J from RS geometry. The argument assembles path closure, per-flip phase, and per-generation Berry sums.

claimOn the three-cube $Q_3$, a discrete transport path is a tick-indexed sequence of vertex states. The canonical Gray-code cycle is closed and returns to its start. Each edge flip contributes a fixed phase; the Berry phase per full cycle is generation-dependent (via face windings). The raw CP phase is the imbalance of these Berry phases and is nonzero.

background

Recognition Science places quark mixing on the three-cube $Q_3$ with its eight-tick Gray-code Hamiltonian cycle. The cycle operator is the unitary on $\mathbb{C}^8$ induced by that directed walk; face winding numbers assign a signed integer to each square face, pairing faces with generation pairs. Gray-code chirality means the directed cycle distinguishes clockwise from counterclockwise face traversal, which is the geometric seed of CP violation.

This module sits downstream of those foundations and of the CKM-from-cube construction (generation torsion ${0,11,17}$ and chirality signature $[4,2,2]$). It introduces discrete transport paths (one state per tick), the canonical closed path, a constant phase per flip, and Berry phases summed per generation. Constants supply the RS tick $\tau_0=1$.

The local goal is not the full CKM matrix but the single rephasing-sensitive phase that later becomes the Jarlskog invariant.

proof idea

Definition layer first: transport paths, the canonical Gray-code path, and lemmas that it is closed and returns. A constant phasePerFlip is fixed; berryPhasePerCycle sums it around the cycle. Three generation-specialized Berry values are recorded and shown to be generation-dependent via the face-winding data. The raw CP phase is assembled from that imbalance; a short theorem records that it is nonzero. No deep analytic machinery: path algebra plus the already-proved chirality and winding signs.

why it matters in Recognition Science

CP violation in the quark sector is measured by the Jarlskog invariant $J_{\mathrm{CP}}\approx 3.08\times 10^{-5}$. The downstream module JarlskogInvariant imports this derivation to obtain the structural form of $J$ from $Q_3$ geometry. Upstream, Gray-code chirality and face windings supply the directed asymmetry; the eight-tick octave (forcing step T7) fixes the cycle length on which Berry phases accumulate.

Without a nonzero raw CP phase tied to generation-dependent windings, the RS account of CKM would be real-orthogonal and CP-conserving. This module closes that gap and hands a concrete phase object to the Jarlskog assembly.

scope and limits

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (19)