ckm_cp_phase
plain-language theorem explainer
The declaration defines the CP-violating phase δ in the CKM matrix as exactly π/2. It encodes the two-tick shift within the eight-tick cycle that produces maximal orthogonality between complex states. Physicists deriving the Jarlskog invariant from cubic ledger topology cite this value to fix sin δ = 1. The definition is a direct assignment with no further reduction steps.
Claim. The CP-violating phase δ is defined by δ = π/2.
background
The MixingDerivation module derives CKM and PMNS elements from overlaps of 8-tick windows on the cubic ledger. Edge-dual coupling fixes generation mixing while the 8-tick closure enforces unitarity. The CP phase is the global phase increment after two ticks, each contributing π/4, so that δ = π/2 yields the largest imaginary part in the Jarlskog invariant.
proof idea
Direct definition that sets the phase to Real.pi / 2. It implements the two-tick shift stated in the module documentation for the eight-tick cycle.
why it matters
This supplies the sin δ = 1 factor inside jarlskog_pred, which is unfolded in jarlskog_pos, jarlskog_match and jarlskog_witness_pos. It completes the geometric account of CP violation inside the Recognition framework's eight-tick octave (T7). The downstream theorems use the fixed phase to match the observed Jarlskog invariant within 20 percent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.