GenerationPhases
plain-language theorem explainer
GenerationPhases assigns fixed phases 0, π/2, and π/4 to the three quark generations. Flavor physicists deriving CKM elements from 8-tick sectors would cite this when building the mixing matrix. The declaration is a direct structure definition that sets the phase fields to values taken from the eight-tick phase map.
Claim. The phases for the three quark generations are assigned as $gen1 = 0$, $gen2 = π/2$, $gen3 = π/4$, matching the 8-tick sectors for (up, down), (charm, strange), and (top, bottom) respectively.
background
The CKM module derives the 3×3 unitary mixing matrix from φ-quantized angles tied to the 8-tick phase structure. Upstream, the phase definition in EightTick supplies the map k ↦ kπ/4 for k in Fin 8, periodic with period 2π. This structure specializes those phases to the generations, with mixing stated to occur between adjacent sectors. The module setting targets a paper deriving CKM parameters from golden-ratio geometry.
proof idea
The declaration is a structure definition that directly initializes the three phase fields with the listed real constants. It imports the phase construction from EightTick and the phase map from the RiemannHypothesis.Wedge module but performs no further computation.
why it matters
This definition supplies the phase inputs needed for the CKM matrix construction in the same module. It realizes the 8-tick octave (T7) for quark flavor mixing and connects to the forcing chain at the level of phase sectors. No downstream theorems are recorded, leaving open the explicit passage from these phases to the Wolfenstein parameters and the α^{-1} band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.