CWPrerequisite
plain-language theorem explainer
The CW boundary prerequisite is the proposition that any coupling profile on Q₃ which couples faces must also couple edges. It encodes the topological attachment rule that 2-cells attach along 1-cells, so face-only coupling is geometrically incoherent. Downstream torsion-forcing theorems cite it to drop the illegal profile and leave exactly three admissible profiles, yielding torsion values {0, 11, 17}. The body is a one-line implication on the two Boolean fields of the profile.
Claim. A coupling profile $p$ (pair of Booleans: edges coupled, faces coupled) satisfies the CW prerequisite when $p$ couples faces only if it also couples edges: $\mathrm{faces}(p)=\mathrm{true}\implies\mathrm{edges}(p)=\mathrm{true}$.
background
The module derives generation torsion values ${0,11,17}$ as the unique schedule compatible with the 8-tick Hamiltonian cycle on the 3-cube $Q_3$, the Recognition Composition Law, and the $\varphi$-ladder. Coupling is tracked only on the nontrivial surface CW levels: edges (dimension 1) and faces (dimension 2). Vertices are already visited by the cycle; the 3-cell interior is not a surface coupling channel.
A coupling profile is therefore a pair of Booleans (edges_coupled, faces_coupled). In the CW decomposition of $Q_3$, every 2-cell is attached along a nonempty 1-skeleton: each square face has four boundary edges. The module doc states this as a topological fact, not a dynamical assumption: "A coupling state that includes faces MUST include edges."
That forces admissible profiles to be a down-set in the CW poset of levels. The illegal profile is faces-on/edges-off; the three survivors are uncoupled, edges-only, and edges-plus-faces.
proof idea
Definitional, not a proof. The predicate is the pure implication p.faces_coupled = true → p.edges_coupled = true on the two fields of CouplingProfile. A DecidablePred instance is inferred by unfolding and the Boolean decidability instance, so the predicate can be used in simp/decide arguments downstream.
why it matters
This is step (C) of the module derivation chain: the CW boundary prerequisite forces level ordering and restricts profiles to a lower set. It is the filter used by cw_prerequisite_forces_three, which proves exactly three profiles survive: $\langle\mathrm{false},\mathrm{false}\rangle$, $\langle\mathrm{true},\mathrm{false}\rangle$, $\langle\mathrm{true},\mathrm{true}\rangle$. From those, admissible_torsion_values obtains torsion ${0,11,17}$ via passive edge/face counts on $Q_3$.
faces_without_edges_violates_cw and six_is_not_admissible record that the eliminated profile would have given $\tau=6$, which is thereby excluded. RCLForcedTorsion requires every generation profile to satisfy the prerequisite and to climb the filtration in dimensional order. The certificate TorsionForcingCert lists ¬ CWPrerequisite ⟨false, true⟩ as one of five independently proved ingredients tying RCL uniqueness (T5), the eight-tick cycle (T7), and $D=3$ (T8) to the mass-ladder torsion schedule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.