pith. machine review for the scientific record. sign in
theorem proved term proof high

ckm_from_phase_overlap

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 158theorem ckm_from_phase_overlap :
 159    Fintype.card (Fin 3 × Fin 3) = 9 := by decide

proof body

Term-mode proof.

 160
 161/-- The Cabibbo angle θ_C ≈ 13° emerges from φ-structure. -/

depends on (2)

Lean names referenced from this declaration's body.