CKMElement
plain-language theorem explainer
CKMElement packages the mixing between the three fermion generations as a complex amplitude indexed by pairs of generation labels. Flavor physicists would cite it when deriving CKM matrix elements from overlaps of 8-tick phase patterns. The declaration is a direct record definition with three fields and no computational reduction.
Claim. A CKM matrix element consists of a source generation index $i$ in the set of three generations, a target generation index $j$ in the same set, and a complex amplitude $V_{ij} in mathbb{C}$.
background
The module derives the existence of exactly three fermion generations from the 8-tick cycle combined with three-dimensional space. The 8-tick cycle supplies eight discrete phases given by $k pi / 4$ for $k = 0$ to $7$, while the three spatial dimensions supply three orthogonal directions. Generations arise as the distinct parity combinations of the phase bits across those directions. Upstream, the tick is the fundamental RS time quantum equal to 1 in native units, and the phase function supplies the periodic 8-tick angles used for overlap calculations.
proof idea
The declaration is a plain structure definition that introduces the record type with fields for source generation, target generation, and complex amplitude.
why it matters
This definition supplies the data structure needed to express CKM mixing as phase overlaps within the three-generation structure. It supports the module's target of deriving generation number from the 8-tick octave (T7) and three spatial dimensions (T8). The parent result is the overall hypothesis that 8 = 2^3 phases distribute across 3D space to produce exactly three generations. It leaves open the explicit computation of numerical mixing angles from the phase overlaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.