CubeGenerationFiltration
plain-language theorem explainer
A Prop-structure packaging the sharpest geometric account of charged-generation torsion: three generation slots, identified with the three independent Q₃ loops/face-pairs, with torsion rising by a passive-edge step then a face step. Mass and excitation-ordering developments cite it as the filtration interface. It is a pure structure definition bundling three component propositions, not a proved theorem.
Claim. A torsion schedule $\tau:\{\mathrm{gen}_1,\mathrm{gen}_2,\mathrm{gen}_3\}\to\mathbb{Z}$ has the cube-generation filtration when (i) the generation slot count equals $3$, (ii) that count equals the number of independent loops on the $3$-cube $Q_3$, and (iii) $\tau$ is incremental cube torsion in dimension $D=3$: $\tau(\mathrm{gen}_1)=0$, $\tau(\mathrm{gen}_2)-\tau(\mathrm{gen}_1)$ equals the passive-edge count of $Q_3$, and $\tau(\mathrm{gen}_3)-\tau(\mathrm{gen}_2)$ equals the face count of $Q_3$.
background
The Generation Torsion Bridge module is the geometric source of truth for charged-generation torsion ${0,11,17}$ on the $D=3$ cube $Q_3$. Spatial dimension is fixed at $D=3$ (T8/T9). The schedule is built from cube combinatorics alone: ground generation carries no geometric coupling; the second generation is edge-dressed by the passive-edge count $E_{\mathrm{passive}}(D)=\mathrm{cube_edges}(D)-1=11$; the third adds the face count, $W_{\mathrm{endo}}(D)=11+6=17$.
IncrementalCubeTorsion is the algebraic, label-free form of that premise: zero at ground, first jump equal to passive edges, second jump equal to faces. The present structure adds two counting identities: generation slots equal three, and those slots unify with the three independent $Q_3$ loops/face-pairs from the winding-charge side.
The module upgrades hardcoded numerals to an explicit structural premise with uniqueness. What remains open is deriving the filtration from the Recognition Composition Law / cost functional rather than taking the ground/edge/face coupling as geometric input. A stronger CW-filtration route appears in ExcitationOrdering.
proof idea
No proof body: this is a structure (Prop bundle), not a theorem. It declares three fields that a schedule $\tau$ must satisfy: equality of generation slot count with $3$; equality of that count with WindingCharges.independent_loop_count 3; and membership in IncrementalCubeTorsion D (ground zero, edge increment, face increment). Downstream theorems construct instances fieldwise (e.g. generationTorsion_has_cube_filtration fills the three fields from slot-count lemmas and generationTorsion_incremental).
why it matters
This is the interface object for the cube-generation story of fermion torsion. generationTorsion_has_cube_filtration shows the canonical schedule carries the package; cubeFiltration_forces_canonical shows any schedule with the package equals canonical torsion, so the filtration is a uniqueness predicate. ExcitationOrdering lifts the same package along the CW route (cwTorsion_has_filtration, excitation_ordering_implies_filtration) and folds it into excitation_ordering_certificate. TorsionForcing uses it as the target of RCL-forced torsion (rcl_forced_implies_filtration).
In the RS chain it sits under $D=3$ (T8) and the eight-tick/cube combinatorics that feed the mass ladder. The doc-comment is explicit that the filtration is still a geometric premise, not yet forced from the cost functional; closing that gap is the remaining open step this package isolates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.