CouplingProfile
plain-language theorem explainer
A two-bit coupling profile on the cube graph Q₃ records whether the 1-skeleton (edges) and 2-skeleton (faces) participate in generation torsion. Level-0 vertices are already fixed by the 8-tick Hamiltonian cycle; the interior is excluded from surface coupling. Downstream torsion theorems enumerate the four Bool pairs and retain only the CW-admissible ones. The declaration is a plain structure with decidable equality; no proof content.
Claim. A coupling profile is a pair of booleans $(e,f)$ stating whether edges (CW dimension 1) and faces (CW dimension 2) of the 3-cube $Q_3$ are coupled. Vertices (dimension 0) are already coupled by the Hamiltonian cycle; the 3-cell interior is not a surface-coupling channel.
background
The module derives generation torsion values ${0,11,17}$ as the unique integers compatible with the 8-tick Hamiltonian cycle on $Q_3$, the Recognition Composition Law, and the $\varphi$-ladder. RCL in log-coordinates becomes d'Alembert; independent coupling channels therefore add in the ladder exponent.
The Gray cycle visits all 8 vertices of $Q_3$ in 8 ticks. At each tick one edge is active and the remaining skeleton is passive, partitioned by CW level. Only two nontrivial surface levels remain: edges (dim 1) and faces (dim 2). Vertices are already locked by the cycle; the interior is unavailable for surface coupling.
CW attachment supplies the ordering constraint used later: every 2-cell is glued along 1-cells, so face coupling without edge coupling is geometrically incoherent. That prerequisite is stated on this profile type, not assumed as dynamics.
proof idea
No proof: this is a structure definition. Two boolean fields (edges_coupled, faces_coupled) with derived DecidableEq and Repr. Downstream code pattern-matches on the four inhabitants and filters by the CW prerequisite proposition.
why it matters
This type is the discrete configuration space for torsion forcing. all_profiles lists the four Bool pairs; CWPrerequisite drops faces-without-edges; cw_prerequisite_forces_three proves exactly three survivors; profileTorsion sums passive edge/face counts for the coupled levels; admissible_torsion_values shows those three profiles yield exactly ${0,11,17}$.
That triple is the generation-torsion set the module claims is forced by 8-tick geometry $\times$ RCL $\times$ $\varphi$-ladder (module chain steps A–E). It sits under the eight-tick octave (T7) and $D=3$ (T8): face-pair count equals $D=3$, matching independent loop count $D(D-1)/2=3$. Without a finite, enumerable profile type, the uniqueness argument cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.