cubeGeoTorsion_third_eq
plain-language theorem explainer
At the third charged generation, cube-geometric torsion equals RecogSpec generation torsion. Both sides reduce to the endogenous face-plus-edge dressing W_endo(D)=E_passive(D)+F(D). Mass and generation authors cite this for the geometric source of τ₃. The proof is a single simp that unfolds both definitions through cube combinatorics at D=3.
Claim. The cube-geometric torsion of the third fermion generation equals the RecogSpec generation torsion of the third generation: both equal the endogenous dressing $W_{\mathrm{endo}}(D)=E_{\mathrm{passive}}(D)+F(D)$, with $E_{\mathrm{passive}}(D)=D\cdot 2^{D-1}-1$ and $F(D)=2D$ at the forced spatial dimension $D=3$.
background
The module GenerationTorsionBridge is the single geometric source of truth for charged-generation torsion ${0,11,17}$. It builds the schedule only from $D=3$ cube combinatorics: ground generation carries no geometric coupling; second generation is edge-dressed by passive field edges; third generation is face-plus-edge dressed.
Upstream constants fix the arithmetic. Spatial dimension $D=3$ is the T8/T9 value. Cube edges are $D\cdot 2^{D-1}$; faces are $2D$. Active edges per tick equal $1$ (one edge transition by T2), so passive field edges are $\mathrm{cube_edges}(D)-1$. For $D=3$ that is $12-1=11$. Endogenous third-generation torsion is then $W_{\mathrm{endo}}(D)=E_{\mathrm{passive}}(D)+\mathrm{cube_faces}(D)=11+6=17$.
cubeGeometricTorsion is the geometric schedule; generationTorsion is the RecogSpec representation. This lemma is the third-generation point of their pointwise agreement.
proof idea
Term-mode proof by a single simp that unfolds both sides. On the geometric side it expands cubeGeometricTorsion at .third into W_endo, then W_endo into passive_field_edges + cube_faces. On the RecogSpec side it expands generationTorsion at .third to the same expression. The remaining constants (cube_edges, active_edges_per_tick, cube_faces, D) reduce by definition, so both sides become identical natural-number terms and the equality closes.
why it matters
Closes the third-generation clause of the bridge that certifies geometric torsion against every other codebase representation. The module's charter is: no raw numerals in cubeGeometricTorsion; pointwise equality with Anchor/Integers.tau; pointwise equality with RecogSpec.generationTorsion; and a uniqueness predicate CubeAdmissibleTorsion whose only solution is this schedule.
Framework landmarks: T8 forces $D=3$; the eight-tick/Q₃ combinatorics supply edges and faces; the third rung is face-plus-edge dressing, not a hardcoded 17. The numerical coincidence with Fedorov's wallpaper count is noted elsewhere (W_endo_at_D3) but is not the primary source here.
Remaining premise (module-level): the ground / passive-edge / face+edge assignment rule is still a structural coupling hypothesis, not yet derived from the RCL alone. This lemma does not discharge that premise; it only proves the two named representations agree at generation three once the geometric definitions are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.