complementMask
plain-language theorem explainer
Bitwise complement on 4-bit vertex masks of the unit hypercube: flip every coordinate bit via XOR with 15. Orbit-classification and flat-Hessian assembly cite it as the generator that pairs Kuhn simplices and swaps hinge types (i,j) with (j,i). The body is a one-line abbreviation of Nat.xor.
Claim. For a natural number $m$ interpreted as a vertex mask in the unit $4$-cube, the complement mask is $m \oplus 15$ (bitwise XOR with the all-ones $4$-bit word).
background
The module classifies triangle hinges inside one Freudenthal/Kuhn triangulation of the unit $4$-cube. Vertices are labeled by $4$-bit masks in ${0,\ldots,15}$; a Kuhn simplex is an ordered $5$-tuple of such masks forming a monotone chain under bit inclusion.
Difference masks of a triangle are the successive XORs along that chain. Their popcounts determine the hinge type $(|a|,|b|)\in{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. The module already imports the $24$ Kuhn simplices and the $15$-class edge-stencil utilities; it does not redefine them.
Complement is the remaining discrete symmetry: XOR every mask with $15=2^4-1$. It reverses the monotone chain and is the nontrivial element of the $\mathbb{Z}/2$ factor in the triangulation-preserving group $S_4\rtimes{id,\mathrm{complement}}$.
proof idea
Pure definition: unfold to Nat.xor m 15. No lemmas, no tactics. Downstream proofs (e.g. edge-mask preservation) expand the definition and cancel the two factors of $15$ by associativity and involution of XOR.
why it matters
Complement is the discrete involution that halves the orbit count of triangle hinges. With it, types $(1,2)\sim(2,1)$ and $(1,3)\sim(3,1)$ merge, leaving four lattice orbits under $S_4\rtimes{id,\mathrm{complement}}$ instead of six under $S_4$ alone.
It feeds complement_preserves_kuhn (every Kuhn vertex-set maps to another in the same cell, with reversed index order) and complement_preserves_edge_mask in the flat-Hessian assembly (edge differences are invariant under simultaneous complement of both endpoints). Those facts are combinatorial prerequisites for assembling the flat $4$D Regge Hessian from per-orbit star kernels; they do not yet evaluate kernels or prove Einstein-Hilbert recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.