profileTorsion
plain-language theorem explainer
Total generation torsion for a coupling profile is the sum of passive subcell counts on the coupled CW levels of the 3-cube. Edges contribute the passive-field count 11; faces contribute the six cube faces. Anyone deriving the forced schedule {0, 11, 17} cites this additive map. The body is a two-branch integer sum of the passive-at-level table.
Claim. For dimension $d$ and a coupling profile $p$ (boolean flags for edge and face coupling on $Q_3$), the profile torsion is $\tau(d,p) = \mathbf{1}_{\mathrm{edges}}(p)\,N_{\mathrm{pass}}(d,1) + \mathbf{1}_{\mathrm{faces}}(p)\,N_{\mathrm{pass}}(d,2)\in\mathbb{Z}$, where $N_{\mathrm{pass}}(d,1)$ is the passive edge count and $N_{\mathrm{pass}}(d,2)$ is the face count under the 8-tick cycle.
background
The module derives the generation torsion values ${0,11,17}$ as the unique integers compatible with the 8-tick Hamiltonian cycle on the 3-cube $Q_3$, the Recognition Composition Law, and the $\varphi$-ladder. RCL in log-coordinates forces independent coupling channels to add in the ladder exponent, so torsion is an integer sum over coupled CW levels.
A coupling profile records which nontrivial surface levels of $Q_3$ are coupled: edges (CW-dim 1) and faces (CW-dim 2). Vertices are already covered by the cycle; the interior 3-cell is not a surface channel. The CW boundary prerequisite further requires that face coupling imply edge coupling, so admissible profiles form a lower set in the CW poset.
Passive-at-level supplies the integer weights: level 1 equals the passive field edges (one active edge per tick leaves 11 passive), level 2 equals the six faces of the cube, and other levels contribute 0. Those weights are the summands of profile torsion.
proof idea
Definitional construction, not a proof. Cast the passive-at-level values at CW levels 1 and 2 to $\mathbb{Z}$, gate each by the corresponding boolean of the coupling profile, and add. No lemmas are invoked; simplification later uses the concrete table passiveAtLevel (edges $\mapsto$ passive field edges, faces $\mapsto$ cube faces).
why it matters
This is the additive map that turns admissible coupling profiles into the torsion schedule. Downstream, the ground profile evaluates to 0, edges-only to 11, and edges-plus-faces to 17; together they feed admissible_torsion_values, which states that every CW-prerequisite profile yields exactly one of ${0,11,17}$.
It is the witness map inside RCLForcedTorsion and generationTorsion_is_rcl_forced, matching the three particle generations to the three lower-set profiles. The face-only profile is excluded by the CW prerequisite; evaluating this map on it yields 6, which lies outside ${0,11,17}$ and is used by cw_prerequisite_is_essential to show the prerequisite is load-bearing.
Framework landmarks: RCL additive composition in the $\varphi$-ladder exponent (module part A), the eight-tick octave on $Q_3$ (T7), and $D=3$ (T8) fixing the passive counts 11 and 6. The construction closes the structural gap between the Gray cycle geometry and the generation torsion integers used in the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.