cubeGeoTorsion_third
plain-language theorem explainer
The third charged-generation geometric torsion equals the endogenous wallpaper integer W_endo at spatial dimension D. Mass-ladder and generation-bridge arguments cite it when matching cube geometry to the {0,11,17} schedule. The equality is definitional: the third slot of the cube torsion map is built as that cast integer, so the proof is reflexivity.
Claim. Cube-geometric torsion on the third fermion generation equals $W_{\mathrm{endo}}(D)$ as an integer, where $D=3$ is the forced spatial dimension and $W_{\mathrm{endo}}(D)=E_{\mathrm{passive}}(D)+F(D)$ is passive cube edges plus cube faces.
background
The Generation Torsion Bridge module fixes charged-generation torsion from $Q_3$ cube combinatorics alone, with no raw numerals in the schedule. Generation 1 (ground) carries torsion 0; generation 2 (edge-dressed) carries the passive-edge count $E_{\mathrm{passive}}(D)=\mathrm{cube_edges}(D)-1$; generation 3 (face+edge-dressed) carries $W_{\mathrm{endo}}(D)=E_{\mathrm{passive}}(D)+F(D)$.
Here $D=3$ is the spatial dimension forced by the T8 step of the forcing chain. Upstream, $W_{\mathrm{endo}}(d)$ is defined as passive field edges plus cube faces; at $D=3$ one has $11+6=17$, which numerically matches the classical wallpaper-group count, though the primary source in this module is the cube sum $E_{\mathrm{passive}}+F$, not the crystallographic coincidence.
The cube schedule is the single geometric source of truth; later lemmas equate it pointwise to Anchor tau values and to RecogSpec generation torsion.
proof idea
One-line term proof by rfl. By construction of the cube-geometric torsion map, the third-generation constructor is definitionally the integer cast of $W_{\mathrm{endo}}(D)$. No rewriting or arithmetic lemmas are required; Lean sees the two sides as the same term.
why it matters
Closes the third slot of the geometric schedule that the module advertises as the authoritative derivation of charged-generation torsion ${0,11,17}$. Together with the first- and second-generation siblings and the values/equality lemmas, it underwrites the claim of no hardcoded numerals and agreement with every other torsion representation in the codebase.
Framework landmarks: $D=3$ from T8; the endogenous third-generation integer $W_{\mathrm{endo}}(3)=17$ that feeds mass-ladder rung structure. The module still treats the ground / passive-edge / face+edge coupling rule as a structural premise (CubeAdmissibleTorsion), not yet derived from the Recognition Composition Law; this lemma only certifies the third geometric value once that assignment is granted. No downstream users are recorded on the graph yet; the intended consumers are the pointwise match lemmas and any mass formula that reads generation torsion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.