gen12_mixing_largest
plain-language theorem explainer
The theorem states that the largest quark mixing in the CKM matrix occurs between the first and second generations because their phase difference is π/2. Particle physicists deriving CKM parameters from Recognition Science foundations would cite this result as the starting point for Cabibbo-angle dominance. The proof is a one-line trivial assertion that the claim holds.
Claim. In the Recognition Science derivation of the CKM matrix, the mixing between the first and second quark generations is the largest (Cabibbo angle) because the phase difference between these generations is exactly π/2.
background
The module derives the full 3×3 CKM matrix from φ-quantized mixing angles tied to the 8-tick phase structure. The 8-tick phases are defined as kπ/4 for k = 0 to 7, with the fundamental time quantum given by tick = 1 in RS-native units. Upstream results supply the phase definition from the EightTick module and the tick constant from Constants, which together set the discrete phase lattice used for flavor mixing.
proof idea
The proof is a one-line wrapper that applies trivial to assert the statement directly.
why it matters
This declaration supplies the initial step in the CKM matrix construction within the StandardModel.CKMMatrix module, linking the 8-tick asymmetry (T7) to the largest 1-2 mixing. It supports the module's target of obtaining CKM elements from φ-angles and feeds the subsequent treatment of the CP-violating phase η that appears in V_ub and V_td. The result touches the paper proposition on CKM matrix from golden ratio geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.