first_increment_is_passive_edges
plain-language theorem explainer
The jump in CW cumulative torsion from the first to the second filtration stage equals the passive field-edge count of the D-cube (11 when D=3). Mass and generation-torsion arguments cite it to pin the first nontrivial excitation as edge-supported. The proof is a one-line simplification unfolding the cumulative torsion and passive-coupling definitions.
Claim. For spatial dimension $D=3$, the difference of CW cumulative torsion between the second and first filtration stages equals the passive field-edge count: $\tau_{\mathrm{CW}}(D,\mathrm{second})-\tau_{\mathrm{CW}}(D,\mathrm{first})=E_{\mathrm{passive}}(D)\in\mathbb{Z}$, where $E_{\mathrm{passive}}(D)$ is the number of cube edges minus the single active edge per tick.
background
The module derives fermion generation torsion ordering from the CW-filtration of the 3-cube $Q_3$. The 0-skeleton has 8 vertices, the 1-skeleton adds 12 edges of which 11 are passive field edges, and the 2-skeleton adds 6 faces. Under the premise that generation excitations couple to subcells in order of CW dimension, the cumulative torsion schedule is ${0,11,17}$: ground couples only to the 0-skeleton ($\tau=0$), the first excitation adds 1-cells ($\tau=11$), and the second adds 2-cells ($\tau=17$).
Spatial dimension is the forced constant $D=3$ (T8/T9). Passive field edges are defined as total cube edges minus the one active edge per tick; for $D=3$ this evaluates to 11, the standard RS dressing count. Cumulative CW torsion is assembled from the passive-coupling weights of the subcells admitted up to each filtration stage.
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 comparison is downstream of the present identity.
proof idea
Term-mode one-liner. Unfold cwCumulativeTorsion and passiveCoupling via simp; the difference of the two cumulative stages reduces definitionally to the passive-coupling contribution of the edge skeleton, which is exactly passive_field_edges D cast to $\mathbb{Z}$. No external lemmas are required beyond those definitional equalities.
why it matters
This identity is the arithmetic content of "first nontrivial excitation is edge-supported." It feeds directly into excitation_ordering_holds, which packages the full ExcitationOrderingTheorem: edge dimension strictly below face dimension, CW torsion matching the canonical generation-torsion schedule, ground cost zero, and edge excitation strictly cheaper in J-cost than the face-supported step.
In the broader RS chain it explains why the CubeAdmissibleTorsion labels (ground/edge/face) are not arbitrary mode names: they are the CW dimensions of $Q_3$ under the filtration principle. The passive-edge count 11 is the same integer that appears in the alpha-derivation dressing sector and in the generation gap structure. The remaining open premise, stated in the module doc, is that excitations do couple in CW-dimension order; this lemma discharges only the numerical increment once that premise is granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.