cwTorsion_second
plain-language theorem explainer
On the 3-cube, cumulative CW-filtration torsion for the second fermion generation equals 11, the passive edge count. Anyone checking the edge-before-face generation schedule or the canonical torsion triple {0,11,17} cites this. The proof is a one-line native_decide evaluation of the closed-form definition at D=3.
Claim. At spatial dimension $D=3$, the cumulative CW-filtration torsion assigned to the second generation equals $11$: $\tau_{\mathrm{CW}}(D,\mathrm{gen}\,2)=11$.
background
The module derives fermion generation torsion from the CW-filtration of the $D=3$ cube $Q_3$. Subcells are ordered by CW dimension: 8 vertices (dim 0), 12 edges of which 11 are passive (dim 1), and 6 faces (dim 2). Generations couple cumulatively to subcells of dimension at most $g-1$.
The schedule function cwCumulativeTorsion encodes that rule: generation 1 gets $\tau=0$; generation 2 adds only the edge passive coupling; generation 3 adds edges plus faces. Spatial dimension $D$ is the constant $3$ forced by the T8 step of the forcing chain (also recovered as T9 linking dimension in the alpha derivation).
Passive edge coupling at $D=3$ is the integer 11. Unfolding the schedule at the second generation therefore reduces to that single integer.
proof idea
One-line computational proof. Unfold cwCumulativeTorsion D .second to the passive edge coupling at $D=3$, then native_decide evaluates the resulting closed Nat/Int expression to 11. No lemmas beyond the definition and the constant $D=3$ are required; the @[simp] attribute exposes the equality to downstream simplifiers.
why it matters
This pins the middle rung of the CW torsion schedule ${0,11,17}$ that the module equates with the canonical generation torsion. Downstream, excitation_ordering_holds packages the full ExcitationOrderingTheorem: edge dimension strictly below face dimension, CW torsion matching the canonical schedule, ground cost zero, and strict J-cost inequality $J(\varphi^{11})<J(\varphi^{17})$.
In the broader framework the integer 11 is the passive 1-skeleton count on the cube forced by $D=3$ (T8). It supplies the geometric reason edges precede faces in CubeAdmissibleTorsion, replacing ad-hoc mode labels by CW dimension. The remaining open premise is the filtration principle itself (excitations couple in CW-dimension order), not this arithmetic identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.