CPPhaseCert
plain-language theorem explainer
Certificate structure that packages five claims: raw CP phase nonzero and positive, generation-dependent Berry phases, CPT balance of the phase, and the strong-CP cost bound. Cited by anyone using the discrete Gray-code derivation of δ_CKM. Pure structure definition; the inhabitant supplies the proofs.
Claim. A CP-phase certificate is a record asserting five properties: the raw CP phase $\delta_{\mathrm{raw}}=\gamma_{\mathrm{Berry}}(0)-\gamma_{\mathrm{Berry}}(1)$ satisfies $\delta_{\mathrm{raw}}\neq 0$ and $\delta_{\mathrm{raw}}>0$; the per-cycle Berry phases of generations $0$ and $1$ differ; $\delta_{\mathrm{raw}}+(-\delta_{\mathrm{raw}})=0$ (CPT balance); and for every real angle $\theta$, $0\le 1-\cos\theta$ (strong-CP cost minimized at vanishing $\theta$).
background
This module derives the CKM CP-violating phase from geometric (Berry) phase accumulated by generation eigenstates on the directed 8-tick Gray-code cycle. For generation $g$, the discrete Berry phase is the sum of overlap arguments around the cycle; here it collapses to bit-flip count on axis $g$ times the elementary flip phase $\pi/4$ from the eight-tick phase ladder.
The raw CP phase is the difference of generation-0 and generation-1 Berry phases, equaling $\pi-\pi/2=\pi/2$. Chirality of the Gray code (unequal flip counts on different axes) forces generation dependence and hence a nonzero $\delta$. CPT balance is the elementary identity that the phase and its negative sum to zero, matching the upstream fact that the J-cost treats $x$ and $x^{-1}$ equally.
The module's key distinction: $\theta_{\mathrm{QCD}}$ is energetic and is driven to zero by J-cost minimization, while $\delta_{\mathrm{CKM}}$ is topological and stays nonzero from directed cycle geometry. That split resolves strong CP without erasing weak-sector CP violation.
proof idea
No proof body: this is a structure packing five Prop fields. Downstream, a single inhabitant fills each field by named lemmas: nonzero and positive from the chirality theorems on the raw phase; generation dependence from the Berry-phase comparison; CPT by a one-line ring identity on $\delta+(-\delta)$; strong CP by the cosine cost bound minimized at zero angle.
why it matters
Gives a single typed bundle for the module's main claims so downstream code can demand "CP phase certified" rather than five separate hypotheses. The sole use site is the verified inhabitant that wires cp_phase_nonzero, cp_phase_positive, berryPhase_generation_dependent, a ring proof of CPT balance, and theta_qcd_cost_minimized_at_zero.
In the Recognition framework this sits on the eight-tick octave (T7) and Gray-code chirality: directed 8-cycle transport supplies a topological $\delta_{\mathrm{CKM}}$ while J-cost forces $\theta_{\mathrm{QCD}}\to 0$. It records the paper-level split between energetic strong-CP resolution and geometric weak CP violation, without yet inserting the full three-generation CKM combination with corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.