Pith. sign in
module module moderate

IndisputableMonolith.StandardModel.CKMFromCube

show as:
view Lean formalization →

Derives CKM mixing suppressions from torsion gaps between quark generations on the 3-cube. Generation overlaps are fixed by Gray-code cycle geometry and mass/weak bases, yielding hierarchical |V_ij| exponents without free Yukawa textures. Particle theorists cite it for structural CKM angles; cosmologists import it for Jarlskog and η_B. The module is mostly explicit gap and flip-weight definitions plus hierarchy lemmas.

claimOn the generation space induced by $Q_3$, torsion gaps $\Delta_{12}$, $\Delta_{13}$, $\Delta_{23}$ between mass eigenstates determine CKM suppression exponents. Flip weights on directed Gray-code edges sum to a fixed total; the hierarchy $\Delta_{12}<\Delta_{23}<\Delta_{13}$ forces $|V_{us}|\gg|V_{cb}|\gg|V_{ub}|$ in $\varphi$-native units, with the CKM matrix the overlap of mass and weak bases.

background

Recognition Science builds the Standard Model gauge group and fermion generations from the 3-cube $Q_3$ and its 8-tick Gray-code cycle. The cycle operator is the unitary on $\mathbb{C}^8$ induced by that directed walk; Gray-code chirality distinguishes orientation and is the geometric source of CP violation. Gauge structure $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ is read off cube automorphisms.

Mass and weak eigenstates are two orthonormal bases on generation space: mass states from CW-level coupling to passive subcells, weak states from the $\mathrm{SU}(2)$ action. Their overlap is the CKM matrix. This module isolates the torsion gaps between generations (the discrete mismatch costs along the $\varphi$-ladder) and the flip weights that grade those gaps, so mixing angles become geometric suppressions rather than free parameters.

Upstream imports supply $\tau_0$, the $J$-cost, torsion forcing, and the cycle/gauge/chirality stack. Local objects named in the module include torsion gaps $12,13,23$, a hierarchy lemma, suppression exponents, and flip-weight sum/value identities.

proof idea

Definition-heavy module with supporting lemmas, not a single end-to-end theorem. It introduces torsionGap and the three pairwise gaps, proves the hierarchy among them, then defines suppressionExponent and the three channel suppressions as functions of those gaps. Flip weights on cube edges are defined, with sum and explicit-value lemmas that pin the discrete grading. Downstream CKM magnitudes and phases consume these numbers; the argument shape is: fix gaps from torsion forcing and cycle geometry, convert gaps to $\varphi$-exponents, verify consistency of flip weights.

why it matters in Recognition Science

Places CKM hierarchy on the same $Q_3$ footing as gauge group and eight-tick dynamics (T7 octave, D=3). Feeds four parents: JarlskogInvariant (structural $J_{\mathrm{CP}}$ from geometry), CPPhaseDerivation (Berry phase of the directed Gray cycle as $\delta_{\mathrm{CKM}}$), BaryonAsymmetryDerivation (sign of $\eta_B$ from $J_{\mathrm{CP}}>0$ plus Sakharov), and EtaBExactRungDerivation (integer rung $-44$ routes that need the same mixing/CP stack). Without torsion-gap suppressions, CKM angles remain phenomenological; with them, quark mixing is a cube-derived prediction used by both SM and cosmology modules.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (22)