six_is_not_admissible
plain-language theorem explainer
The coupling profile with faces on and edges off yields torsion 6 on the 3-cube, and is ruled out by the CW boundary prerequisite. Anyone proving uniqueness of generation torsions {0, 11, 17} cites this exclusion. The proof is a two-component term: a simp evaluation of profile torsion against cube_faces and D, paired with the faces-without-edges lemma.
Claim. For spatial dimension $D = 3$, the coupling profile with edges off and faces on has profile torsion equal to $6$, and it fails the CW prerequisite (if faces are coupled then edges must be coupled).
background
The module derives generation torsion values ${0, 11, 17}$ as the unique values compatible with the 8-tick Hamiltonian cycle on the 3-cube $Q_3$, projected onto the $\varphi$-ladder through the Recognition Composition Law. Independent couplings add in the ladder exponent because RCL forces $J = \cosh - 1$ and multiplicative composition of arguments.
A coupling profile records which CW levels of $Q_3$ are active. Profile torsion counts passive subcells at those levels. The CW prerequisite is the attachment rule: face coupling requires edge coupling, since every 2-cell of $Q_3$ is attached along 1-cells (four boundary edges per face). Profiles that couple faces without edges are topologically incoherent.
Here $D = 3$ (forced spatial dimension) and $\mathrm{cube_faces}(D) = 2D = 6$. The profile $\langle \mathrm{edges}=\mathrm{false},, \mathrm{faces}=\mathrm{true}\rangle$ is the unique candidate that would produce torsion 6.
proof idea
Term-mode pair constructor for the conjunction.
Left conjunct: simp unfolds profileTorsion and passiveAtLevel at the faces-only profile, reduces against cube_faces and D, and obtains $6$.
Right conjunct: apply faces_without_edges_violates_cw, which discharges $\neg,\mathrm{CWPrerequisite},\langle\mathrm{false},\mathrm{true}\rangle$ directly from the definition (faces coupled implies edges coupled fails when edges are off).
why it matters
Closes one exclusion cell in the torsion-forcing chain of this module: among conceivable passive-subcell counts on $Q_3$, $\tau = 6$ arises only from faces-without-edges, which CW attachment forbids. The surviving admissible profiles are then assigned to the three fermion generations (ground, edges, edges+faces), matching face-pairs$(D) = 3$ and the landmark $D = 3$ from the forcing chain (T8).
The module header states the goal as uniqueness of ${0, 11, 17}$ from 8-tick cycle $\times$ RCL $\times$ $\varphi$-ladder; this theorem removes the spurious sixth face-only channel. No downstream consumers are wired yet (used_by empty), but the Part 6 generation-assignment block immediately below treats the admissible set as settled once such exclusions hold. Ties to T7 (eight-tick octave on $Q_3$) and the CW filtration ordering used for Gen 2 vs Gen 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.