cubeGeoTorsion_second_eq
plain-language theorem explainer
Pointwise equality for the second charged generation: cube-geometric torsion equals ledger generation torsion. Both sides reduce to the passive-edge count of the D=3 cube (11). Anyone matching geometric and RecogSpec torsion schedules cites this. Proof is a single simp unfolding both definitions through cube combinatorics.
Claim. The cube-geometric torsion of the second charged generation equals the recognition-ledger generation torsion of that generation: $\tau^{\mathrm{geo}}(\mathrm{second}) = \tau^{\mathrm{gen}}(\mathrm{second})$. Explicitly both equal the passive field-edge count $E_{\mathrm{passive}}(D)=D\cdot 2^{D-1}-1$ at $D=3$.
background
The Generation Torsion Bridge module is the single authoritative source for charged-generation torsion ${0,11,17}$ from $Q_3$ cube geometry, and proves it matches every other representation in the codebase. The schedule is pure $D=3$ combinatorics: gen 1 (ground) has $\tau=0$; gen 2 (edge-dressed) has $\tau=E_{\mathrm{passive}}(D)$; gen 3 (face+edge) has $\tau=W_{\mathrm{endo}}(D)=E_{\mathrm{passive}}+F$.
cubeGeometricTorsion assigns those branches with no raw numerals: second generation is (passive_field_edges D : ℤ). Passive field edges are total cube edges minus the single active edge per tick (T2): cube_edges d - 1 with cube_edges d = d·2^(d-1). Spatial dimension $D=3$ is forced by T8/T9. The ledger side generationTorsion is the RecogSpec schedule this module certifies against pointwise.
proof idea
One-line term proof by simp. Unfolds cubeGeometricTorsion on .second to the cast of passive_field_edges D, unfolds generationTorsion on .second to the same integer, then reduces passive_field_edges, cube_edges, active_edges_per_tick, and D to matching numerals. No case split or arithmetic lemma beyond definitional equality.
why it matters
Fills the second-generation clause of the module's certification that cube geometry agrees with RecogSpec.generationTorsion (item 3 of "What This Module Certifies"). Together with the first- and third-generation siblings and the bundled pointwise equality, it upgrades the torsion schedule from hardcoded numerals to an explicit cube-combinatorial definition with matching ledger values.
Framework landmarks: $D=3$ from the forcing chain (T8), active-edge-per-tick from T2, and the edge-dressed second generation as $E_{\mathrm{passive}}(3)=11$. The remaining open premise is the structural coupling rule in CubeAdmissibleTorsion (ground / passive-edge / face+edge modes), not yet derived from the RCL alone; this lemma does not close that premise, only the numeral-free geometric–ledger match for gen 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.