passiveCoupling
plain-language theorem explainer
Assigns to each CW subcell type of the D-cube the number of sites available for passive coupling: 0 on vertices, passive field edges on edges, and all 2D faces on faces. Anyone deriving the generation-torsion schedule {0, 11, 17} from the cube filtration cites this map. It is a pure case split on subcell type with no proof obligations.
Claim. For each natural number $d$, the passive-coupling count on subcells of the $d$-cube is $0$ at a vertex, the number of passive field edges (total edges minus one active edge) at an edge, and the face count $2d$ at a face.
background
The module builds fermion generation torsion from the CW-filtration of the spatial 3-cube $Q_3$. Subcells relevant to coupling are typed as vertices (CW-dim 0), edges (dim 1), and faces (dim 2). The filtration premise is that successive generations couple to successive skeletons, so the torsion increments are exactly the passive counts at each new dimension.
Upstream constants fix those counts: passive field edges equal total cube edges minus one active edge per tick (11 when $D=3$), and the face count is $2d$ (6 when $D=3$). Vertices contribute nothing because the ground state couples trivially. The definition packages those three numbers as a single function of subcell type, so cumulative torsion can be written without case-by-case constants.
proof idea
Definition by exhaustive pattern match on the three constructors of the subcell inductive type. Vertex maps to 0; edge maps to the imported passive-field-edge count; face maps to the imported face count $2d$. No tactics, lemmas, or arithmetic beyond the upstream definitions.
why it matters
This is the numerical spine of the CW route to generation torsion. Cumulative torsion is defined by summing these values: generation 1 gets 0, generation 2 adds the edge count, generation 3 adds the face count, recovering the schedule ${0,11,17}$ at $D=3$. Downstream theorems then prove that schedule equals the canonical generation torsion, that the first increment is exactly the passive edges, that edges are the minimal nontrivial excitation by CW dimension, and that the full excitation-ordering certificate holds (including strict $J$-cost ordering $J(\varphi^0)<J(\varphi^{11})<J(\varphi^{17})$).
In the broader framework this supplies the geometric reason edges precede faces in cube-admissible torsion: it is the CW-dimensional order on $Q_3$ (T8 forces $D=3$), not an ad hoc mode label. The remaining open premise is the filtration principle itself (excitations couple in CW-dimension order), which this definition does not discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.