complementMask
plain-language theorem explainer
Bitwise vertex complement on the unit 4-cube: flip the four coordinate bits of a vertex mask by XOR with 15. Cited wherever dual star types (2,1)↔(1,2) and (3,1)↔(1,3) must share edge-class data. The body is the one-line definition m ↦ m ⊕ 15.
Claim. Define the vertex complement on natural-number masks by $C(m) := m \oplus 15$, i.e. flip the lowest four bits. This is the geometric antipode map inside the unit 4-cube whose vertices are labeled by bitmasks in $\{0,\ldots,15\}$.
background
In the 4D Regge campaign, vertices of the unit hypercube are labeled by 4-bit masks $0..15$. Edges, triangles, and Kuhn simplices are encoded as sets of those masks. The module assembles the flat zero-momentum Hessian of the 4D Regge action from committed per-orbit star-deficit kernels and Heron area gradients, replacing the provisional weight-1 stencil.
The complement $m \mapsto m \oplus 15$ is the antipodal map on the 4-cube: it sends each vertex to the opposite corner. Upstream, the orbit-classification module introduces the same map and proves it carries Kuhn simplex vertex-sets to Kuhn simplex vertex-sets (after reversing the monotone chain). Because difference masks satisfy $(u\oplus 15)\oplus(v\oplus 15)=u\oplus v$, edge-class indices are invariant under complement.
That invariance is the bridge between dual $S_4$ orbit types: type-(2,1) kernels equal the committed type-(1,2) kernels on $\mathrm{Fin},15$, and likewise for (3,1)↔(1,3).
proof idea
Pure definition: one-line abbreviation of Nat.xor m 15. No proof obligations. Downstream lemmas unfold it and apply XOR associativity/commutativity (e.g. complement preserves edge masks via $(u\oplus 15)\oplus(v\oplus 15)=u\oplus v$).
why it matters
Complement transport is deliverable A.2 of the flat Hessian assembly: it lets the module reuse committed type-(1,2) and (1,3) star kernels for the dual types without recomputing geometry. Parent results include complement_preserves_edge_mask (identity on edge-class indices) and, in the orbit module, complement_preserves_kuhn (Kuhn simplices map to Kuhn simplices).
Those facts feed the zero-momentum true-weight Hessian: the orbit-count-weighted sum of $(dA\cdot c)(d\delta\cdot c)$ over the six $S_4$ types with counts 72/48/48/24/24/24. Evaluations on pure-gauge decoys then vanish, whereas provisional weight-1 did not. Scope remains zero-momentum per-cell Hessian; finite-momentum Bloch folding and full $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence stay open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.