generationSlotCount_eq_loopCount
plain-language theorem explainer
The number of charged-generation slots equals the count of independent loops on the 3-cube Q₃. Mass and generation-torsion arguments cite this to identify combinatorial generation capacity with cube winding data. The proof unfolds the slot count and rewrites via the D=3 face-pair/loop equality.
Claim. The generation slot count equals the number of independent loops on the spatial 3-cube: $\mathrm{generationSlotCount} = N_{\mathrm{loops}}(Q_3)$. Equivalently, the slot inventory coincides with the independent face-pair count forced at $D=3$.
background
The Generation Torsion Bridge module derives the charged-generation torsion schedule ${0,11,17}$ from $D=3$ cube combinatorics rather than raw numerals. Spatial dimension is fixed at $D=3$ by the forcing chain (T8/T9). On the 3-cube $Q_3$, independent closed windings and opposite face-pairs are the natural geometric carriers of generation structure.
Generation slots are the discrete capacity for charged generations supported by that cube. Upstream winding-charge results identify the independent loop count at dimension 3 with the face-pair count on $Q_3$. The module's packing comment states the present surface claim sharply: the cube contributes exactly three generation slots, and those slots coincide with the three independent $Q_3$ loops/face-pairs.
Torsion itself still accumulates by an edge increment then a face increment; this lemma only equates the slot inventory to the loop inventory.
proof idea
Term-mode, essentially a one-step rewrite. Unfold the definition of the generation slot count, then apply simpa with the constant $D=3$ against the symmetric form of WindingCharges.loops_eq_face_pairs_D3, which already equates independent loops on $Q_3$ with face-pairs at dimension three. No arithmetic casework remains after that identification.
why it matters
This is the loop/face-pair unification leg of the cube-generation filtration package. Downstream, generationTorsion_has_cube_filtration installs it as loop_facepair_unification beside the three-slot count and the incremental torsion steps, packing "the current strongest structural explanation of charged-generation torsion."
It is also the bridge in minimalLoopExcitation_matches_generation_slots: any minimal loop-excitation profile that exhausts the cube loops is forced to match the generation slot count via this equality.
In the broader RS picture it ties generation capacity to $D=3$ cube geometry (T8) and to winding charges on $Q_3$, upgrading hardcoded generation counts to an explicit geometric identity. What remains open, as the module states, is deriving the ground/edge/face coupling rule from the cost functional (RCL) rather than taking the filtration as a geometric premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.