cwTorsion_incremental
plain-language theorem explainer
The cumulative CW-filtration torsion schedule on the 3-cube is an incremental cube torsion: each generation only adds the newly admitted skeleton layer. Anyone deriving the generation ladder {0, 11, 17} from cube geometry cites this. The proof rewrites to the generation-torsion schedule and applies the already-proved incremental property there.
Claim. With spatial dimension $D = 3$, the cumulative CW-filtration torsion schedule $\tau_{\mathrm{CW}}$ (generation 1 maps to $0$, generation 2 to the passive edge coupling, generation 3 to edge plus face coupling) satisfies the incremental cube-torsion property: successive generations add only the newly opened skeleton layer.
background
The module builds fermion generation ordering from the CW-filtration of the 3-cube $Q_3$. The 0-skeleton has 8 vertices, the 1-skeleton adds 12 edges (11 passive), and the 2-skeleton adds 6 faces. Spatial dimension is the forced value $D = 3$ (T8/T9).
The schedule cwCumulativeTorsion assigns torsion by cumulative skeleton depth: generation 1 couples only to the empty filtration ($\tau = 0$); generation 2 opens the 1-cells and adds the passive edge coupling; generation 3 opens the 2-cells and adds the face coupling. That yields the integer ladder ${0, 11, 17}$ in $D = 3$.
IncrementalCubeTorsion is the filtration package asserting that each successive generation only charges the newly admitted layer. An upstream bridge lemma already proves the same property for the canonical generation-torsion schedule; a sibling equality identifies the CW schedule with that one.
proof idea
Term-mode one-liner. Rewrite the goal along the sibling equality that identifies CW cumulative torsion with generation torsion, then discharge by the upstream lemma generationTorsion_incremental from GenerationTorsionBridge, which already establishes the incremental cube-torsion property for the generation schedule.
why it matters
This closes the incremental half of the CW-filtration package for generation torsion. The module's larger claim is that IF excitations couple to $Q_3$ subcells in CW-dimension order, THEN the first nontrivial excitation is edge-supported, the next is face-supported, the torsion schedule matches the canonical ${0, 11, 17}$, and J-cost is strictly monotone on the corresponding $\varphi$-powers: $J(\varphi^0) = 0 < J(\varphi^{11}) < J(\varphi^{17})$.
The geometric fact dim 1 < dim 2 supplies the structural reason edges precede faces, replacing ad-hoc mode labels in CubeAdmissibleTorsion by a single filtration principle. No downstream consumers are wired yet; the immediate sibling is the full filtration-package theorem that packages this incremental fact with the rest of the cube-generation axioms. The remaining open premise is the coupling principle itself (excitations follow CW dimension), still a structural hypothesis rather than a derived law. Landmarks in play: T8 forcing $D = 3$, the eight-tick cube, and the $\varphi$-ladder mass/torsion bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.