Pith. sign in
module module moderate

IndisputableMonolith.StandardModel.CPPhaseDerivation

show as:
view Lean formalization →

Derives the CP-violating phase from Berry phases along the canonical Gray-code transport path on the Q₃ cube. Generation-dependent face windings give distinct phases for the three generations and a nonzero raw CP phase. Anyone linking cube chirality to the Jarlskog invariant cites this module. The argument builds closed-path returns, a per-flip phase, and generation-indexed Berry sums.

claimOn the 3-cube $Q_3$, a discrete transport path is a tick-indexed sequence of vertex states. The module fixes a canonical Gray-code cycle, proves it is closed and returns to its start, assigns a phase per bit-flip and a Berry phase per generation cycle $\Phi_g$ ($g=1,2,3$), assembles a raw CP phase $\delta_{\mathrm{CP}}$ from those data, and proves $\delta_{\mathrm{CP}}\neq 0$.

background

Recognition Science places quark mixing on the Boolean 3-cube $Q_3$. The eight-tick Gray-code cycle induces a unitary cycle operator on $\mathbb{C}^8$ and a directed walk that is chiral: clockwise and counterclockwise face traversals are inequivalent. Face winding numbers pair faces with generation pairs; that chirality is the geometric source of CP violation.

Upstream, CKM-from-cube already builds the mixing matrix from generation torsion ${0,11,17}$ and chirality signature $[4,2,2]$. Constants fix the RS time quantum $\tau_0=1$ tick. This module supplies the missing phase layer: discrete transport paths (one state per tick), the canonical closed path, a phase per flip, and generation-dependent Berry phases along that cycle.

proof idea

Definition-first module, then short lemmas. It introduces transport paths and a canonical Gray-code path; proves the path is closed and returns; defines a phase per bit-flip and a Berry phase per cycle; specializes to three generation Berry values; records that those values are generation-dependent; packages a raw CP phase and proves it is nonzero. Geometric input (signed windings, chirality) is imported from FaceWinding and GrayCodeChirality; directed dynamics from CycleOperator.

why it matters in Recognition Science

Sole recorded consumer is JarlskogInvariant, which takes the structural CP phase and forms the rephasing-invariant $J_{\mathrm{CP}}=\mathrm{Im}(V_{us}V_{cb}V_{ub}^V_{cs}^)$ from the same $Q_3$ ingredients. The module is the bridge from Gray-code chirality and face windings to a concrete nonzero $\delta_{\mathrm{CP}}$ that the Jarlskog layer can quote. It sits on the eight-tick octave and $D=3$ landmarks: the path lives on $Q_3$ with period $2^3$. Without a proved nonzero raw phase, the geometric CP story stops at chirality and never reaches the measured invariant.

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)