faces_without_edges_violates_cw
plain-language theorem explainer
The coupling profile that turns faces on while leaving edges off fails the CW boundary prerequisite on Q₃. Anyone deriving admissible generation torsions from the 8-tick skeleton cites this to kill the τ = 6 candidate. The proof is a one-step absurdity: the implication faces⇒edges applied to that Boolean pair yields false = true.
Claim. The coupling profile with edges off and faces on does not satisfy the CW boundary prerequisite: face coupling does not imply edge coupling for $\langle \mathrm{edges}=\bot,\,\mathrm{faces}=\top\rangle$, so $\neg(\mathrm{faces}\Rightarrow\mathrm{edges})$ holds for that pair.
background
The module derives the generation torsion set ${0,11,17}$ as the only values compatible with the 8-tick Hamiltonian cycle on the 3-cube $Q_3$, projected onto the $\varphi$-ladder through the Recognition Composition Law. Passive subcells of the cycle are counted by CW level (edges vs faces); each admissible coupling profile sums those passive counts into a torsion exponent.
A coupling profile is a Boolean pair (edges coupled?, faces coupled?). The CW prerequisite encodes the attachment rule of the cube complex: every 2-cell is glued along 1-cells, and each face of $Q_3$ has four boundary edges. Formally the predicate is $p_{\mathrm{faces}}=\mathrm{true}\Rightarrow p_{\mathrm{edges}}=\mathrm{true}$. Profiles that couple faces without edges would make the face boundary invisible, which is topologically incoherent.
This sits in step (C) of the module chain: after RCL additivity of torsion channels and the Gray-cycle partition of $Q_3$, the CW lower-set condition cuts the Boolean lattice of profiles down to the admissible ones.
proof idea
Pure Boolean case analysis, no geometric lemmas. Assume the CW prerequisite holds for $\langle\mathrm{false},\mathrm{true}\rangle$. Unfolding the implication and feeding the hypothesis $\mathrm{faces}=\mathrm{true}$ (by reflexivity) forces $\mathrm{edges}=\mathrm{true}$. That contradicts $\mathrm{edges}=\mathrm{false}$, discharged by decide. The whole argument is intro then absurd.
why it matters
This is the topological veto that removes the only remaining non-generation torsion. Downstream, six_is_not_admissible packages the arithmetic fact that the outlawed profile would give $\tau=6$ together with this negation, so $\tau=6$ never enters the admissible set. The same lemma is wired into torsion_forcing_certificate as the cw_prerequisite field of the certificate structure that asserts uniqueness of the schedule ${0,11,17}$.
In the broader RS chain this is the concrete content of module step (C): CW attachment on $Q_3$ forces coupling profiles to be downward-closed in the edge–face poset. Combined with the 8-tick passive counts (step B), RCL additivity on the $\varphi$-ladder (step A, landmark T5/RCL), ground-state zero torsion (step D), and the three face-pair generation slots forced by $D=3$ (step E, landmark T8), only the three generation torsions survive. Without this veto the certificate would admit a spurious fourth rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.