generationSlotCount_eq_three
plain-language theorem explainer
At spatial dimension three the cube supplies exactly three generation slots. Anyone citing the charged-generation torsion schedule {0, 11, 17} or the cube-filtration package needs this equality first. The proof is a one-line simplification that identifies the slot-count definition with the opposite-face-pair count at D = 3.
Claim. The number of generation slots equals $3$. Equivalently, the slot count coincides with the number of opposite face pairs of the $3$-cube (and with the number of independent $Q_3$ loops).
background
The module derives charged-generation torsion ${0, 11, 17}$ from $Q_3$ cube combinatorics alone, with no raw numerals in the geometric schedule. Spatial dimension is fixed at $D = 3$ by the forcing chain (T8/T9). Generation slots are the discrete places at which fermion generations couple to cube features: ground, passive-edge, and face+edge modes.
Upstream, face_pairs counts opposite face pairs of the $D$-cube; at $D = 3$ that count is exactly three by definitional reduction. The same integer is the number of independent $Q_3$ loops. The slot-count definition is written so that it equals this face-pair count once $D$ is substituted.
Locally this is the first brick of the cube-generation filtration: slot count, loop/face-pair unification, and incremental torsion steps must all hold before the schedule is certified admissible.
proof idea
One-line term-mode wrapper. Unfold the slot-count definition and the constant $D$, then apply ParticleGenerations.face_pairs_at_D3, which is the reflexivity proof that face_pairs 3 = 3. simpa closes the goal.
why it matters
Feeds directly into generationTorsion_has_cube_filtration, which packages slot count, loop/face-pair unification, and incremental torsion into the full CubeGenerationFiltration structure on the canonical schedule. That structure is how the module certifies agreement with Anchor integers and RecogSpec torsion without hardcoded numerals.
Framework landmark: three generations from $D = 3$ (T8 forces spatial dimension three; opposite face pairs of the cube then force three slots). The module still treats the ground / passive-edge / face+edge assignment rule as a structural premise, not yet derived from the Recognition Composition Law; this lemma only locks the cardinality of the slot set. A stronger ordering route appears in ExcitationOrdering via the CW-filtration of $Q_3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.