profileTorsion_edges_faces
plain-language theorem explainer
For spatial dimension D = 3, the coupling profile that activates both edges and faces has torsion equal to 17. Mass and generation analyses cite this as the top rung of the admissible torsion set {0, 11, 17}. The proof is a one-line simplification that unfolds the profile torsion formula into passive field edges plus cube faces and evaluates the cube counts at D = 3.
Claim. With spatial dimension $D = 3$, the torsion of the coupling profile that includes both edges and faces equals $17$: $\mathrm{profileTorsion}(D,(\mathrm{edges},\mathrm{faces})) = 17$. Equivalently, passive field edges plus cube faces evaluate to $11 + 6 = 17$.
background
The module derives generation torsion values ${0, 11, 17}$ as the unique set compatible with the 8-tick Hamiltonian cycle on the 3-cube $Q_3$, projected onto the $\varphi$-ladder through the Recognition Composition Law. RCL forces independent couplings to add in the ladder exponent, so torsion is a sum of passive subcell contributions by CW level.
Cube geometry is fixed by the forced dimension $D = 3$: $\mathrm{cube_edges}(D) = D \cdot 2^{D-1} = 12$ and $\mathrm{cube_faces}(D) = 2D = 6$. One edge is active per atomic tick, so passive field edges equal $12 - 1 = 11$. The CW attachment order (faces attach along edges) restricts admissible coupling profiles to downward-closed subsets of the CW poset: ground (nothing), edges only, or edges and faces.
Profile torsion at a level is the sum of passive contributions from all included levels. The edges-and-faces profile therefore totals passive edges plus faces.
proof idea
Term-mode simp unfolds profileTorsion at the edges-and-faces profile into the sum of passiveAtLevel contributions, then rewrites those via passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, and D. Numerically: passive edges $= 3 \cdot 2^{2} - 1 = 11$, faces $= 2 \cdot 3 = 6$, total $17$. No external lemmas beyond the constant definitions are required.
why it matters
This is the edges-and-faces evaluation that closes the top value in the admissible torsion triple. Downstream, admissible_torsion_values cases on the three CW-prerequisite profiles and quotes this fact for the $\langle\mathrm{true},\mathrm{true}\rangle$ branch, obtaining exactly ${0, 11, 17}$.
In the forcing chain the result sits at the junction of T7 (eight-tick octave on $Q_3$), T8/$D = 3$, and RCL additivity of ladder exponents. The module narrative treats ${0, 11, 17}$ as the structural generation-torsion spectrum once variational ground cost forces the zero profile and CW lower-set structure limits the rest. Without the $17$ evaluation the uniqueness claim for the three admissible profiles would be incomplete.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.