generationTorsion_incremental
plain-language theorem explainer
The charged-generation torsion schedule satisfies the incremental cube filtration: ground torsion is zero, the first jump equals the passive-edge count, and the second jump equals the face count of the D-cube. Mass and excitation-ordering arguments cite this as the algebraic form of that structural premise. The proof is a one-line transfer of already-proved cube admissibility across the admissibility–incremental equivalence.
Claim. For spatial dimension $D=3$, the canonical generation torsion $\tau:\{\mathrm{gen}_1,\mathrm{gen}_2,\mathrm{gen}_3\}\to\mathbb{Z}$ obeys $\tau(\mathrm{gen}_1)=0$, $\tau(\mathrm{gen}_2)-\tau(\mathrm{gen}_1)=E_{\mathrm{passive}}(D)$, and $\tau(\mathrm{gen}_3)-\tau(\mathrm{gen}_2)=F_{\mathrm{cube}}(D)$.
background
The Generation Torsion Bridge module is the geometric source of truth for charged-generation torsion ${0,11,17}$. It builds the schedule from $D=3$ cube combinatorics alone: gen 1 (ground) has no geometric coupling; gen 2 is edge-dressed by the passive-edge count $E_{\mathrm{passive}}(D)=\mathrm{cube_edges}(D)-1=11$; gen 3 adds the face count, $W_{\mathrm{endo}}(D)=11+6=17$. Spatial dimension $D=3$ is the T8-forced value used throughout.
Incremental cube torsion is the label-free restatement of cube admissibility. It keeps only cumulative step data: ground at zero torsion, first jump equal to the passive-edge count, second jump equal to the face count. The module treats this as a more algebraic packaging of the same structural premise about how fermion generations couple to cube features.
Cube admissibility of the canonical schedule is already available in-module; an equivalence theorem identifies that predicate with the incremental two-step filtration. This declaration simply exports the incremental form.
proof idea
One-line term proof. Apply the left-to-right direction of the in-module equivalence between cube admissibility and incremental cube torsion at $D$ and the canonical schedule, feeding the already-proved admissibility of that schedule. No new arithmetic is performed.
why it matters
This is the algebraic handle on the generation-torsion premise used by the rest of the mass stack. Downstream, the CW cumulative torsion inherits the same filtration by rewriting to the canonical schedule and citing this result; the full cube-generation filtration package records these torsion steps as one of its fields; and RCL-forced torsion is reduced to the incremental predicate by uniqueness plus this theorem.
In framework terms it sits on T8 ($D=3$) and the cube-arithmetic derivation of ${0,11,17}$, not on the wallpaper-group coincidence. The module is explicit that the ground / passive-edge / face+edge assignment rule remains a structural premise until derived from the Recognition Composition Law; this theorem upgrades the gap from hardcoded numerals to an explicit uniqueness-ready filtration, which ExcitationOrdering then strengthens via CW subcell dimension and J-cost ordering on $\varphi$-power ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.