cpPhaseCert
plain-language theorem explainer
Packages the CP-phase derivation as a single certificate: raw δ_CKM is nonzero and positive, generation Berry phases differ, CPT holds algebraically, and the Strong-CP cost is minimized at θ=0. Cite it when claiming RS separates topological weak CP violation from energetic θ_QCD. The body is a structure instance wiring five prior lemmas (one field by ring).
Claim. There is a verified CP-phase certificate asserting: the raw CP phase $\delta$ satisfies $\delta \neq 0$ and $\delta > 0$; the discrete Berry phases of generations $0$ and $1$ differ; $\delta + (-\delta) = 0$; and for every real $\theta$, $0 \le 1 - \cos\theta$ (J-cost penalty for nonzero $\theta_{\mathrm{QCD}}$ vanishes only at zero).
background
The module derives the CKM CP phase from Berry phase accumulated by generation eigenstates on the directed 8-tick Gray-code cycle. For a generation state $|\psi_g\rangle$, $\gamma_{\mathrm{Berry}}(g)$ is the argument of the product of consecutive overlaps around the cycle; $\delta_{\mathrm{CKM}}$ is a fixed combination of those generation phases (plus corrections). Nonzero $\delta$ comes from Gray-code chirality, generation-dependent coupling to $Q_3$ levels, and directed traversal breaking time-reversal.
The certificate structure bundles five claims: raw phase nonzero and positive; Berry phases of the first two generations unequal; algebraic CPT on the raw phase; and the Strong-CP inequality $0 \le 1-\cos\theta$ for all real $\theta$. Upstream, cp_phase_nonzero and cp_phase_positive reduce the raw combination of gen-1/gen-2 Berry values to $\pi$-positivity; berryPhase_generation_dependent is the same inequality at the level of per-cycle phases. The Strong-CP field is the J-cost fact that any $\theta\neq 0$ raises effective cost via $1-\cos\theta$.
Local convention: $\theta_{\mathrm{QCD}}$ is energetic and minimized by J-cost; $\delta_{\mathrm{CKM}}$ is topological and forced nonzero by cycle geometry. That split is the module's stated resolution of Strong CP while retaining weak CP violation.
proof idea
Structure instance, not a deep proof. Four fields are direct citations: nonzero and positive raw phase from cp_phase_nonzero and cp_phase_positive; generation dependence from berryPhase_generation_dependent; Strong CP from theta_qcd_cost_minimized_at_zero (which is cos_le_one plus linarith). The CPT field is discharged in place by ring on $\delta+(-\delta)=0$. No new arithmetic beyond those lemmas.
why it matters
Closes the module's certificate layer for CP-phase derivation: one object that a downstream Standard Model assembly can require instead of five separate lemmas. It records the framework split between topological $\delta_{\mathrm{CKM}}$ (Berry phase on the directed eight-tick Gray cycle, T7 octave) and energetic $\theta_{\mathrm{QCD}}$ (J-cost minimum at zero, T5 J-uniqueness lineage). No used_by edges yet; the value is packaging for later CKM/CP assembly and for the paper claim that Strong CP is resolved without killing weak CP violation. Chirality of the Gray code and generation-dependent Berry phases are the physical content; the certificate only freezes that content into a checkable record.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.