cubeGeoTorsion_second
plain-language theorem explainer
Second-generation charged torsion equals the passive-field edge count of the D-cube, cast to integers. Mass and generation-bridge authors cite it to unfold the geometric schedule without numerals. The proof is pure definitional equality (rfl) from the case split of cubeGeometricTorsion.
Claim. The cube-geometric torsion assigned to the second charged generation equals the number of passive field edges of the $D$-cube, viewed as an integer: $\tau_{\mathrm{geo}}(\mathrm{gen}_2) = E_{\mathrm{passive}}(D) \in \mathbb{Z}$.
background
The module GenerationTorsionBridge is the geometric source of truth for charged-generation torsion ${0, 11, 17}$. It defines the schedule entirely from $Q_3$ cube combinatorics at the forced spatial dimension $D = 3$ (T8/T9), with no literal integers in the definition.
cubeGeometricTorsion sends generation labels to integers: ground (first) gets $0$; second gets the passive-field edge count; third gets the endogenous face+edge weight $W_{\mathrm{endo}}(D)$. Passive field edges are total cube edges minus the single active edge per tick, so they are the edges that dress the interaction. Upstream docs fix $D := 3$ and record that for $D=3$ the passive count is $11$.
The local claim is the second branch of that definition, exposed as a simp fact so downstream equalities can reduce generation-two torsion to cube arithmetic.
proof idea
One-line definitional proof. The second case of cubeGeometricTorsion is written exactly as (passive_field_edges D : ℤ), so rfl closes the equality. No lemmas are applied beyond the definition and the integer cast.
why it matters
This lemma is the second rung of the geometric torsion schedule that replaces hardcoded generation gaps with cube combinatorics. Together with the first- and third-generation siblings it underwrites pointwise agreement with Anchor tau values and RecogSpec generationTorsion, and feeds the uniqueness story for the CubeAdmissibleTorsion predicate.
In the RS chain, $D=3$ is forced (T8), and passive edges at that dimension give the classic second-generation integer $11$ used on the phi-ladder mass formula. The module still treats the ground / passive-edge / face+edge coupling rule as a structural premise until it is derived from the RCL; this simp fact closes the definitional half of that upgrade for generation two. No downstream users are recorded yet; sibling equalities (cubeGeoTorsion_values, matches against tau) are the intended consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.