profileTorsion_ground
plain-language theorem explainer
The ground coupling profile (neither edges nor faces coupled) contributes zero torsion on the φ-ladder. Anyone deriving the admissible generation torsion set {0, 11, 17} cites this as the zero case of the additive channel sum. The proof is a one-line simplification of the profile-torsion definition at the all-false profile.
Claim. For spatial dimension $D=3$, if the coupling profile has neither edges nor faces coupled, then its torsion equals $0$.
background
The TorsionForcing module derives the generation torsion values {0, 11, 17} as the unique integers compatible with the 8-tick Hamiltonian cycle on the 3-cube, the Recognition Composition Law, and the φ-ladder. Under RCL, independent coupling channels compose additively in the ladder exponent, so total torsion is a sum of passive counts over coupled CW levels.
A coupling profile is a pair of booleans: whether 1-cells (edges) and 2-cells (faces) are coupled. Profile torsion at dimension $d$ is the sum of the passive-at-level counts for those levels that are switched on. Spatial dimension is fixed at $D=3$ by the forcing chain (T8).
The ground profile is the all-false pair: no edges, no faces. Variational dynamics already forces ground-state torsion to zero elsewhere in the mass stack; this lemma records the matching evaluation of the additive definition.
proof idea
One-line wrapper. Unfold the definition of profile torsion and simplify: both boolean guards are false, so each summand is zero and the total is $0$. No external lemmas beyond the definition and the ambient $D$ constant are required.
why it matters
This is the zero branch of admissible_torsion_values, which states that every CW-prerequisite-satisfying profile yields torsion in {0, 11, 17}. That theorem case-splits on the three admissible profiles and dispatches the ground case by this identity.
In the module chain, (A) RCL forces additive torsion channels, (B)–(C) the 8-tick cycle and CW boundary order restrict profiles to a lower set, and (D) the variational ground state sits at zero cost. The lemma pins (D) at the level of the explicit torsion functional. Framework landmarks in play: T7 eight-tick octave, T8 forcing $D=3$, and the RCL additive structure behind the φ-ladder mass formula. It does not itself close uniqueness of the triple; it supplies the ground value that uniqueness theorems quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.