second_gen_is_passive_edges
plain-language theorem explainer
Second-generation geometric torsion equals the passive edge count of the 3-cube: total cube edges minus one active edge per tick. Generation and mass theorists cite it to fix τ₂ from Q₃ combinatorics with no raw numerals. The proof is a one-line simplification that unfolds the torsion schedule and the passive-edge definition.
Claim. The cube-geometric torsion of the second charged fermion generation equals the passive field-edge count of the $D$-cube: $E_{\mathrm{cube}}(D)-1$, where $E_{\mathrm{cube}}(D)=D\cdot 2^{D-1}$, $D=3$ is the forced spatial dimension, and one edge is active per atomic tick.
background
The Generation Torsion Bridge module is the single geometric source of truth for charged-generation torsion ${0,11,17}$. It builds the schedule from $D=3$ cube combinatorics alone: gen 1 (ground) has torsion $0$; gen 2 (edge-dressed) has torsion equal to the passive edge count; gen 3 (face+edge-dressed) adds the face count.
Spatial dimension $D=3$ is forced by the T8 step of the forcing chain. The $D$-cube has $E_{\mathrm{cube}}(D)=D\cdot 2^{D-1}$ edges (so $12$ when $D=3$). By T2 there is one active edge transition per atomic tick, so the passive (field) edges that dress the interaction are $E_{\mathrm{cube}}(D)-1=11$. The local definition cubeGeometricTorsion assigns each generation its geometric mode without embedding literal integers.
proof idea
Term-mode one-liner. simp unfolds the second-generation clause of the cube-geometric torsion schedule and the definition of passive field edges. Those two unfoldings are definitionally equal to $\uparrow(E_{\mathrm{cube}}(D)-\mathrm{active_edges_per_tick})$, which is the stated right-hand side. No arithmetic or case split is required.
why it matters
This is the explicit bridge step that identifies second-generation torsion with passive edges of $Q_3$, the module's gen-2 clause $\tau_2=E_{\mathrm{passive}}(D)=11$. Together with the sibling equalities for gen 1 and gen 3 it discharges the module's certification goals: no raw numerals in the torsion schedule, and pointwise agreement with Anchor $\tau$ and RecogSpec generation torsion.
Framework landmarks in play are T8 ($D=3$) and the eight-tick / cube geometry that supplies edge counts. The module still carries an explicit structural premise (CubeAdmissibleTorsion): the physical rule that gen 2 couples to passive edges is not yet derived from the Recognition Composition Law alone. Closing that premise is the remaining open question; this lemma only records the combinatorial identity once the coupling mode is granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.