passiveCoupling_vertex
plain-language theorem explainer
Passive coupling on the 0-skeleton of the D-cube vanishes: vertices contribute zero subcells to the torsion count. Anyone deriving the generation torsion schedule {0, 11, 17} from CW filtration cites this as the ground-state base case. The proof is pure definitional equality (rfl).
Claim. For spatial dimension $D=3$, the passive-coupling count of a vertex cell of the cube is $0$.
background
The module builds excitation ordering for fermion generation torsion from the CW-filtration of the 3-cube $Q_3$. Subcells are stratified by dimension: 8 vertices (dim 0), 12 edges (dim 1), 6 faces (dim 2). Generation excitations are assumed to couple in that order, producing the cumulative torsion schedule ${0, 11, 17}$.
Passive coupling counts how many subcells at a given CW level can absorb torsion without being the active transition. By definition it sends vertices to $0$ (ground state couples trivially), edges to $\mathrm{cube_edges}-1$ (one edge is active), and faces to all six faces. Spatial dimension $D$ is fixed at $3$ by the forcing chain (T8/T9).
This lemma is the vertex clause of that definition, specialized at $D$.
proof idea
One-line wrapper: rfl. The definition of passive coupling pattern-matches on the cell constructor and returns $0$ on .vertex, so the equality is definitional and needs no lemmas.
why it matters
It anchors Gen 1 of the torsion schedule: ground-state coupling to the 0-skeleton alone yields $\tau=0$. The module argument then stacks edge and face contributions to reach $\tau=11$ and $\tau=17$, after which J-cost monotonicity on $\varphi$-power ratios gives the strict ordering $J(\varphi^0)=0 < J(\varphi^{11}) < J(\varphi^{17})$.
No downstream theorems currently depend on this simp fact in the graph, but it is the base case that makes the CW-dimensional story replace ad-hoc mode labels in CubeAdmissibleTorsion. The remaining premise of the module (excitations couple in CW-dimension order) is still structural, not derived here. Framework landmarks: T8 forces $D=3$; the eight-tick octave and $\varphi$-ladder sit upstream of the mass/torsion story this module feeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.