all_profiles_complete
plain-language theorem explainer
Every coupling profile on the nontrivial CW levels of Q₃ appears in the fixed four-element enumeration of Boolean pairs (edges coupled, faces coupled). Anyone enumerating admissible torsion channels before the CW filter cites this exhaustiveness fact. The proof is pure case analysis on the two Bool fields after unfolding the list.
Claim. Let $p$ be any coupling profile, i.e. a pair of booleans $(e,f)$ recording whether edges (CW-dim 1) and faces (CW-dim 2) of $Q_3$ are coupled. Then $p$ belongs to the list $\{\langle\mathsf{false},\mathsf{false}\rangle,\langle\mathsf{true},\mathsf{false}\rangle,\langle\mathsf{false},\mathsf{true}\rangle,\langle\mathsf{true},\mathsf{true}\rangle\}$.
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 nontrivial CW levels participate in surface coupling. Vertices (level 0) are already covered by the Hamiltonian cycle; the interior (level 3) is unavailable. That leaves two booleans: edges coupled and faces coupled. The list of all profiles is exactly the four Boolean pairs.
The next step in the chain (not this theorem) imposes the CW boundary prerequisite: faces attach along edges, so face coupling without edge coupling is topologically forbidden. Exhaustiveness of the four-element list is the prerequisite for that filter.
proof idea
Unfold the definition of the four-element list and the list-membership lemmas. Destructure the profile into its two Boolean fields. Case-split on both booleans (four cases). In each case, simp with the structure injectivity equation closes membership. No external lemmas beyond list membership and Boolean exhaustion.
why it matters
This is the enumeration completeness step inside torsion forcing: before the CW lower-set filter can drop $\langle\mathsf{false},\mathsf{true}\rangle$ and leave three surviving profiles, one must know the ambient list is all of $\mathsf{Bool}^2$. The module chain then ties those survivors to passive subcell counts on the 8-tick Gray cycle, additive RCL torsion, and the variational ground state at zero, yielding ${0,11,17}$.
Framework landmarks in play are T7 (eight-tick octave on $Q_3$), T8 ($D=3$), and RCL-driven additive exponents on the $\varphi$-ladder. No downstream theorems currently depend on this declaration in the graph; it is local scaffolding for the profile filter that follows in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.