cwTorsion_first
plain-language theorem explainer
The cumulative CW-filtration torsion for the first fermion generation is zero on the D-cube. Anyone building the edge-before-face generation schedule cites this as the ground-state base case of the torsion ladder {0, 11, 17}. The equality is definitional: the filtration schedule assigns nothing to generation one, so the proof is reflexivity.
Claim. Let $D=3$ be the forced spatial dimension. The cumulative torsion assigned by the CW-filtration schedule of the $D$-cube to the first generation equals $0$.
background
The module derives edge-before-face excitation ordering for fermion generation torsion from the CW structure of the 3-cube $Q_3$, together with J-cost monotonicity on $\varphi$-power ratios. The cube has the standard filtration: 0-skeleton (8 vertices), 1-skeleton (12 edges, 11 passive), 2-skeleton (6 faces).
The cumulative torsion schedule maps generations to integers by coupling each generation to all subcells of CW dimension at most one less than the generation index. Generation one (ground) couples to nothing, so its torsion is defined to be 0; generation two adds edge coupling; generation three adds face coupling. The resulting integers are the familiar ladder ${0, 11, 17}$ when $D=3$.
Here $D$ is the spatial dimension forced by the T8 step of the forcing chain (also recovered as T9 linking dimension in the alpha derivation). The theorem is the ground-state clause of that schedule.
proof idea
One-line definitional proof. The cumulative torsion function is defined by pattern-match on generation, with the first-generation arm equal to the integer literal 0. Unfolding that arm at $D$ yields $0 = 0$ by rfl. The @[simp] attribute exposes the reduction to the simplifier.
why it matters
This is the base case of the CW-derived torsion schedule that replaces ad-hoc mode labels (ground/edge/face) in cube-admissible torsion by a single geometric filtration principle. The module argument is: if excitations couple to $Q_3$ subcells in CW-dimension order, then the first nontrivial excitation is edge-supported, the next is face-supported, and the torsion values match the canonical ladder, with strict J-cost ordering $J(\varphi^0)=0 < J(\varphi^{11}) < J(\varphi^{17})$.
No downstream consumers are wired yet in the graph; the declaration exists so later lemmas can simplify the ground generation away and focus on the edge and face increments. It sits inside the masses domain and inherits $D=3$ from the T8 forcing landmark. The remaining open premise of the module is the filtration principle itself (coupling ordered by CW dimension), which is structural rather than derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.