ratio_Vus_Vcb_structural
plain-language theorem explainer
The absolute torsion gap between generations 2 and 3 is strictly smaller than between generations 1 and 2: |τ₂−τ₁| < |τ₁−τ₀|. CKM hierarchy arguments that compare |V_us| to |V_cb| via φ-suppression cite this inequality. The proof is a one-shot native_decide on the concrete integers from the torsion triple {0,11,17}.
Claim. Let $\tau:\mathrm{Fin}\,3\to\mathbb{Z}$ be the generation torsion with values $\tau(0)=0$, $\tau(1)=11$, $\tau(2)=17$, and write $\Delta\tau(i,j):=\tau(j)-\tau(i)$. Then $|\Delta\tau(1,2)| < |\Delta\tau(0,1)|$.
background
The module derives the CKM quark-mixing matrix from Q₃ cube geometry, generation torsion {0, 11, 17}, and Gray-code chirality [4,2,2]. Mass eigenstates sit at those torsion levels: ground (0), edge-dressed (11), and edge+face-dressed (17). Off-diagonal mass-basis amplitudes are suppressed as $\varphi^{-|\Delta\tau_{ij}|}$, so torsion gaps set the leading hierarchy of mixing strengths.
The local definition torsionGap i j is just the integer difference $\tau_j - \tau_i$. The present statement compares the two adjacent gaps that feed the Cabibbo-scale entries $V_{us}$ (gens 1–2) and $V_{cb}$ (gens 2–3). Full mixing angles also fold in flip-count weights from the weak-basis even-sign-flip generators; this lemma isolates the pure torsion comparison.
Upstream, the only content dependency is that torsion-gap definition. The TraceLogic all edge is incidental bookkeeping, not used in the arithmetic.
proof idea
Term/tactic proof by native_decide. Both sides evaluate to concrete natural numbers: $|\tau_2-\tau_1|=|17-11|=6$ and $|\tau_1-\tau_0|=|11-0|=11$, and $6<11$ is decided by the kernel. No lemmas are invoked beyond the definition of the gap.
why it matters
In the CKM-from-cube program, mixing magnitudes scale as flip-weight times $\varphi^{-|\Delta\tau|}$. Establishing $|\Delta\tau_{23}| < |\Delta\tau_{12}|$ is the torsion half of the structural claim that the $|V_{us}|/|V_{cb}|$ hierarchy has the right order of magnitude (doc-comment: structure correct order; numerical target $\sim 5.5$ observed vs $\sim 7.8$ from $\lambda\approx 0.236$, $A\approx 6/11$).
It sits with the sibling gap and suppression lemmas (gap_12, gap_23, suppression_12, suppression_23, torsionGap_hierarchy) that feed the master CKM structural certificate in Part 7. Framework landmarks: generation torsion on the $\varphi$-ladder and the three-generation Fin-3 space forced by the cube (T7/T8 adjacency). No downstream theorems yet; this is a leaf inequality waiting on the certificate bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.