ckm_from_phase_overlap
plain-language theorem explainer
The theorem counts the nine possible pairs of fermion generations that index CKM matrix elements arising from 8-tick phase overlaps. Flavor physicists modeling mixing angles in the Standard Model would cite this combinatorial step when deriving generation structure from Recognition Science. The proof is a direct decide tactic that evaluates the finite cardinality of the 3-by-3 product set.
Claim. The set of ordered pairs between three fermion generations has cardinality nine: $|G_1, G_2, G_3| ^2 = 9$.
background
The module derives exactly three fermion generations from the 8-tick cycle (period $2^3$) crossed with three spatial dimensions. Each tick phase is indexed by a 3-bit string whose parity assignments label the generations; the nine pairs then label the possible overlaps that define CKM entries. This rests on the upstream result that reduces seven independent axioms to four structural conditions plus three definitional facts.
proof idea
One-line wrapper that applies the decide tactic to compute the cardinality of the finite product set directly.
why it matters
It supplies the 3-by-3 counting step required for the CKM-from-phase-overlap claim in the three-generations module. The result sits inside the T7 eight-tick octave and T8 derivation of D=3, closing the combinatorial prerequisite for the paper proposition on generation number. The module notes the derivation remains speculative pending further checks against observed mixing data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.