cubeGeoTorsion_incremental
plain-language theorem explainer
The canonical cube-geometric generation torsion schedule satisfies the incremental filtration: ground torsion vanishes, the first jump equals the passive-edge count, and the second jump equals the face count. Mass and generation authors cite it when they need the algebraic (label-free) form of the structural premise rather than the mode-labeled admissibility predicate. The proof is a one-line transfer across the proved equivalence between the two formulations.
Claim. For spatial dimension $D=3$, the canonical geometric torsion schedule $\tau$ on the three charged generations satisfies the incremental cube filtration: $\tau(\mathrm{gen}_1)=0$, $\tau(\mathrm{gen}_2)-\tau(\mathrm{gen}_1)=E_{\mathrm{passive}}(D)$, and $\tau(\mathrm{gen}_3)-\tau(\mathrm{gen}_2)=F_{\mathrm{cube}}(D)$.
background
The module Generation Torsion Bridge is the single source of truth for charged-generation torsion ${0,11,17}$ derived from $Q_3$ cube combinatorics. Generation 1 (ground) has zero geometric coupling; generation 2 is edge-dressed by the passive-edge count $E_{\mathrm{passive}}(D)=\mathrm{cube_edges}(D)-1$; generation 3 is face+edge-dressed by $W_{\mathrm{endo}}(D)=E_{\mathrm{passive}}(D)+\mathrm{cube_faces}(D)$. At the forced spatial dimension $D=3$ (T8), these evaluate to $0$, $11$, and $17$.
Two equivalent structural predicates package the same assignment rule. CubeAdmissibleTorsion keeps mode labels (ground / passive-edge / face+edge). The incremental form drops the labels and retains only cumulative steps: ground at zero, first jump equals passive edges, second jump equals faces. The module treats this rule as an explicit structural premise about how fermion generations couple to cube features, not yet a consequence of the Recognition Composition Law alone.
Upstream, $D$ is fixed to $3$ by the forcing chain, and the sibling equivalence theorem states that cube admissibility is equivalent to the incremental two-step filtration for any dimension and any torsion schedule.
proof idea
One-line term proof. Apply the forward direction of the sibling equivalence cubeAdmissible_iff_incremental at $(D,\tau_{\mathrm{geo}})$, then discharge the left-hand side with the already-proved fact that the geometric schedule is cube-admissible. No new arithmetic is performed.
why it matters
This declaration closes the algebraic half of the module's certification list: the geometric schedule is not only mode-admissible but also satisfies the pure increment filtration used by downstream algebraic arguments. Together with pointwise agreement against Anchor integers and RecogSpec generation torsion, it upgrades hardcoded numerals ${0,11,17}$ to a unique solution of an explicit structural predicate built only from cube edge and face counts.
In the broader Recognition framework this sits under the mass/generation layer fed by T8 ($D=3$) and the eight-tick cube geometry. The remaining open premise, stated in the module header, is that the ground/passive-edge/face coupling rule itself has not yet been derived from the RCL or J-cost; ExcitationOrdering offers a stronger CW-filtration route that orders edge before face by subcell dimension. No downstream consumers are currently wired to this specific lemma, so it functions as a certified interface for algebraic callers that prefer increments over mode labels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.