cwTorsion_cubeAdmissible
plain-language theorem explainer
The CW-cumulative torsion schedule on the 3-cube is cube-admissible: it matches the canonical generation torsion values that CubeAdmissibleTorsion demands. Anyone citing the CW-filtration story for fermion generations (edge before face, schedule {0, 11, 17}) needs this bridge. The proof rewrites CW torsion to generation torsion and applies the existing admissibility theorem.
Claim. For spatial dimension $D = 3$, the CW-cumulative torsion schedule on the $D$-cube is a cube-admissible torsion: it satisfies the structural constraints that define admissible generation torsion on $Q_3$ (the canonical schedule arising from coupling in CW-dimension order).
background
The module builds excitation ordering for fermion generation torsion from the CW-filtration of the 3-cube $Q_3$. The 0-skeleton has 8 vertices, the 1-skeleton contributes 11 passive edges, and the 2-skeleton adds 6 faces. Coupling excitations in order of CW dimension yields the cumulative torsion schedule ${0, 11, 17}$: generation 1 stays at the 0-skeleton ($\tau = 0$), generation 2 adds 1-cells ($\tau = 11$), generation 3 adds 2-cells ($\tau = 17$).
Cube-admissible torsion is the predicate that a torsion schedule is the canonical one compatible with that cube geometry (mode labels ground/edge/face, or their CW replacements). Spatial dimension $D$ is fixed at 3 by the forcing chain (T8). The CW-cumulative torsion is the schedule read off the filtration; generation torsion is the same numerical schedule under the generation-bridge identification.
J-cost monotonicity on $\varphi$-power ratios then gives the strict cost order $J(\varphi^0) = 0 < J(\varphi^{11}) < J(\varphi^{17})$, but that step is separate from admissibility itself.
proof idea
Two-line tactic proof. First rewrite the CW-cumulative torsion via the equality that identifies it with generation torsion (cwTorsion_eq_generationTorsion). Then discharge the goal by the already-proved fact that generation torsion is cube-admissible (generationTorsion_admissible). No new arithmetic: pure transport of the admissibility certificate across the CW/generation identification.
why it matters
In the Recognition Masses layer this closes the geometric half of the excitation-ordering argument: once torsion is read from the CW filtration of $Q_3$, it automatically satisfies the cube-admissible interface that the rest of the generation story expects. The module doc states the payoff: IF excitations couple in CW-dimension order, THEN the first nontrivial excitation is edge-supported, the next is face-supported, the torsion schedule equals the canonical one, and J-cost orders it strictly.
That supplies the structural reason edges precede faces, which would otherwise be an unexplained label in cube-admissible torsion. It sits on $D = 3$ (T8) and the eight-tick/cube combinatorics, and feeds the J-cost monotonicity block that follows in the same file. No downstream consumers are wired yet (used_by empty); the remaining premise is still the filtration principle itself (coupling ordered by CW dimension), not a derived theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.