cw_prerequisite_is_essential
plain-language theorem explainer
The face-only coupling profile (edges off, faces on) has torsion outside the forced set {0, 11, 17}. Anyone defending uniqueness of generation torsions cites this exclusion: drop the CW boundary prerequisite and a fourth family with τ = 6 becomes admissible. The proof is a direct simplification of the profile-torsion formula at D = 3 against the face count 2D.
Claim. For spatial dimension $D = 3$, the torsion of the coupling profile with edges inactive and faces active does not belong to the integer set $\{0, 11, 17\}$.
background
The module derives 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 makes independent couplings add in the ladder exponent, so torsion is assembled from passive subcell counts by CW level.
Coupling profiles are pairs of booleans marking which skeleton levels (edges, faces) participate. The CW attachment structure of $Q_3$ forces faces to attach along edges: any face-active state must already include edges. That topological lower-set constraint is the CW prerequisite. Profile torsion evaluates the passive contribution of a given profile; at $D = 3$ one has $\mathrm{cube_faces} = 2D = 6$.
Upstream constants fix $D = 3$ (T8) and the face count $2D$. The Gray-cycle partition of $Q_3$ supplies the passive tallies (1 active edge, 11 passive edges, 6 faces on the skeleton) that feed the admissible profiles.
proof idea
Term-style simp proof. Unfold profileTorsion and passiveAtLevel, substitute cube_faces and D (so $D=3$ and faces $=6$), then discharge non-membership with Set.mem_insert_iff. The face-only profile evaluates to torsion $6$, which is none of $0, 11, 17$. No intermediate lemmas beyond those unfoldings.
why it matters
Documents why the CW prerequisite is load-bearing in the torsion-forcing chain, not optional scaffolding. The module aims to force ${0, 11, 17}$ from the 8-tick cycle $\times$ RCL $\times$ $\varphi$-ladder; without excluding the face-only profile, a fourth family at $\tau = 6$ would survive and the schedule would not be unique. That exclusion is exactly the content of the doc-comment: the CW prerequisite is the reason profile $\langle\mathrm{false},\mathrm{true}\rangle$ is out.
Framework landmarks in play: T7 (eight-tick octave on $Q_3$), T8 ($D=3$), and the RCL additive torsion channels that turn passive subcell counts into ladder exponents. No used_by edges are recorded yet; the result sits as a local essentiality lemma inside Masses.TorsionForcing, supporting the uniqueness narrative rather than feeding a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.