cwTorsion_third
plain-language theorem explainer
At spatial dimension D=3, CW-cumulative torsion for the third generation stage equals 17. Mass and generation-ordering arguments cite this as the face-supported rung of the schedule {0,11,17}. The proof is a one-line native_decide evaluation of the closed combinatorial count on the 3-cube.
Claim. For spatial dimension $D=3$, the CW-cumulative torsion at the third generation stage equals $17$: $\tau_{\mathrm{CW}}(D,\mathrm{third})=17$.
background
The module builds fermion generation torsion from the CW-filtration of the 3-cube $Q_3$. Skeletons are ordered by cell dimension: 8 vertices (dim 0), 12 edges of which 11 are passive (dim 1), and 6 faces (dim 2). Cumulative torsion is then the running sum of passive couplings along that filtration.
The intended schedule is ${0,11,17}$: ground couples only to the 0-skeleton ($\tau=0$); the first excitation adds passive edges ($\tau=11$); the second adds the six faces ($\tau=11+6=17$). Spatial dimension is the forced constant $D=3$ from the T8/T9 chain (linking and cube geometry both require three space dimensions).
This declaration isolates the third-stage value in that schedule. Sibling counts (subcellCount, passiveCoupling on vertices/edges/faces) supply the integers that the cumulative definition folds.
proof idea
Term-mode proof by native_decide. After unfolding cwCumulativeTorsion at $D=3$ and stage .third, the expression reduces to a closed natural-number combination of cube face and passive-edge counts; the kernel decides equality to 17 by computation. No external lemmas are invoked beyond the definitional arithmetic already in scope.
why it matters
Feeds excitation_ordering_holds, which packages the full ordering theorem for $Q_3$: edge dimension below face dimension, CW torsion matching canonical generation torsion, and strict J-cost increase $J(\varphi^0)<J(\varphi^{11})<J(\varphi^{17})$. The value 17 is the face-supported third-generation rung that must match the canonical generationTorsion schedule used elsewhere in the masses layer.
Framework landmarks: T8 forces $D=3$, so the cube (not a higher hypercube) is the correct complex; the eight-tick/octave counting sits upstream of the vertex count $2^D=8$. The remaining structural premise in the module is that excitations couple in CW-dimension order; this lemma does not discharge that premise, only the numerical third-stage entry once the filtration is granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.