second_increment_is_faces
plain-language theorem explainer
The second jump in CW-cumulative torsion (third generation level minus second) equals the face count of the D-cube. Anyone assembling the fermion generation torsion schedule {0, 11, 17} on Q₃ cites this identity. The proof is a one-line simplification that unfolds the cumulative torsion definition and the combinatorial face count.
Claim. For spatial dimension $D$, the CW-cumulative torsion at the third generation level minus that at the second equals the number of faces of the $D$-cube: $\tau_{\mathrm{CW}}(D,3)-\tau_{\mathrm{CW}}(D,2)=2D$ (as an integer).
background
The module builds fermion generation torsion from the CW-filtration of the $D=3$ cube $Q_3$. Subcells are ordered by dimension: 0-skeleton (vertices), 1-skeleton (edges), 2-skeleton (faces). When excitations couple in that order, cumulative torsion is scheduled as ground $\tau=0$, first excitation adding passive field edges, second excitation adding faces.
Here $D=3$ is the spatial dimension forced by the linking argument. The face count is the combinatorial quantity $\mathrm{cube_faces}(D)=2D$ (so 6 for $Q_3$). Passive field edges are total cube edges minus one active edge per tick, giving 11 in $D=3$. CW-cumulative torsion at successive generation levels is built by stacking the passive couplings of those skeletons.
The local claim isolates the second increment only: the face contribution that takes the schedule from the edge-supported level to the face-supported level.
proof idea
Term-mode proof by a single simp that unfolds CW-cumulative torsion, passive coupling, passive field edges, cube edges, active edges per tick, cube faces, and $D$. After unfolding, both sides reduce to the same integer expression $2D$, so the equality is definitional arithmetic rather than a geometric argument.
why it matters
This identity is one brick in the excitation ordering package for $Q_3$. Downstream, excitation_ordering_holds packages the full ExcitationOrderingTheorem, whose clauses include edge-before-face dimensional ordering, equality of CW-cumulative torsion with the canonical generation torsion schedule, and strict J-cost ordering $J(\varphi^0)<J(\varphi^{11})<J(\varphi^{17})$.
Together with the first-increment (passive-edge) identity, it explains why the canonical torsion values are ${0,11,17}$: ground couples only to the 0-skeleton, the first excitation adds the 11 passive edges, and the second adds the 6 faces. That geometric origin replaces ad-hoc mode labels in cube-admissible torsion with a single CW-filtration principle (still a structural premise about coupling order, not a derived dynamical law).
Framework landmarks in view: $D=3$ from the forcing chain, the eight-tick octave as the ambient discrete clock, and J-cost monotonicity on $\varphi$-power ratios that turns the torsion schedule into a strict mass-cost order on the $\varphi$-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.