cubeAdmissible_iff_incremental
plain-language theorem explainer
Cube-admissible generation torsion (ground zero, second generation at passive edges, third at passive edges plus faces) is equivalent to the purely incremental filtration (zero base, first jump by passive edges, second jump by faces). Anyone proving uniqueness of the {0,11,17} schedule from either packaging cites this. The proof is a two-direction structure constructor with ring and rewrites on the mode equations.
Claim. For any dimension $d\in\mathbb{N}$ and any integer-valued generation torsion schedule $\tau$, the following are equivalent: (i) $\tau$ is cube-admissible, i.e. $\tau(\mathrm{gen}_1)=0$, $\tau(\mathrm{gen}_2)=E_{\mathrm{passive}}(d)$, and $\tau(\mathrm{gen}_3)=E_{\mathrm{passive}}(d)+F(d)$; (ii) $\tau$ is incremental cube torsion, i.e. $\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(d)$. Here $E_{\mathrm{passive}}(d)$ is the passive-field edge count and $F(d)=2d$ is the face count of the $d$-cube.
background
The Generation Torsion Bridge module derives charged-generation torsion from $D=3$ cube combinatorics and certifies agreement with every other representation in the codebase. The schedule is Gen 1 (ground): $\tau=0$; Gen 2 (edge-dressed): $\tau=E_{\mathrm{passive}}(D)$; Gen 3 (face+edge-dressed): $\tau=E_{\mathrm{passive}}(D)+F(D)$. At $D=3$ this is ${0,11,17}$, with $E_{\mathrm{passive}}(3)=11$ and $F(3)=6$.
CubeAdmissibleTorsion packages that assignment as absolute mode values: ground zero, second generation equal to passive-field edges, third equal to passive edges plus faces. The module doc stresses this is a structural premise about how fermion generations couple to cube features, not a consequence of the cost functional alone.
IncrementalCubeTorsion is the same premise rewritten as cumulative steps: ground at zero, first jump adds $E_{\mathrm{passive}}(d)$, second jump adds $F(d)=2d$. Upstream, passive_field_edges is total cube edges minus the active edge per tick, and cube_faces is $2d$.
proof idea
Bidirectional constructor on the two structures.
Forward (admissible $\to$ incremental): keep ground_is_zero. For the edge increment, rewrite with ground zero and the absolute edge-mode equation, then ring. For the face increment, rewrite with edge-mode and face+edge-mode, then ring.
Reverse (incremental $\to$ admissible): keep ground_is_zero. Recover absolute edge mode from the edge increment by simpa with ground zero. For absolute face+edge mode, first obtain $\tau(\mathrm{second})=E_{\mathrm{passive}}(d)$ the same way, then expand $\tau(\mathrm{third})=(\tau(\mathrm{third})-\tau(\mathrm{second}))+\tau(\mathrm{second})$, substitute the face increment and that second-generation identity, and finish by ring.
No external lemmas beyond the structure fields and the definitions of passive_field_edges and cube_faces.
why it matters
This equivalence lets the bridge treat mode-labeled admissibility and the algebraic two-step filtration as interchangeable. Downstream, cubeGeoTorsion_incremental and generationTorsion_incremental transport the geometric and RecogSpec schedules into the incremental view via the forward direction. incremental_forces_canonical uses the reverse direction so that any schedule satisfying only the cumulative jumps is forced equal to canonical generationTorsion (via the existing cube-admissible uniqueness theorem).
In the module's certification list this supports the forcing predicate whose unique solution is the canonical schedule, upgrading hardcoded ${0,11,17}$ numerals to an explicit structural premise with uniqueness. Framework context: $D=3$ spatial dimensions (T8) fix $F=6$ and $E_{\mathrm{passive}}=11$, hence third-generation $17$. The remaining open gap is deriving the ground/edge/face coupling rule itself from the Recognition Composition Law; until then the premise stays structural (see also the CW-filtration route in ExcitationOrdering).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.