complement_preserves_kuhn
plain-language theorem explainer
Bitwise complement (XOR 15) of a reversed Kuhn vertex chain is again a Kuhn simplex vertex-set in the same 4-cube cell. Combinatorial gravity and Regge-calculus workers cite it when collapsing hinge types under the triangulation-preserving group. The proof is exhaustive case analysis on the 24 simplices, discharged by decision.
Claim. For every Kuhn simplex index $s \in \{0,\ldots,23\}$ there exists $s'$ such that for each step $i=0,\ldots,4$, the nested Freudenthal vertex mask of $s'$ at $i$ equals the bitwise complement (XOR $15$) of the vertex mask of $s$ at step $4-i$.
background
The module classifies triangle hinges inside one unit 4-cube under the Freudenthal/Kuhn triangulation: 24 oriented 4-simplices whose vertices are nested bit masks in ${0,\ldots,15}$. The API vertexMask s k is the nested Freudenthal vertex after $k$ steps along simplex $s$ (partial sums of the four axis bits in the order fixed by $s$).
Complement inside the cube is the 4-bit flip $m \mapsto m \oplus 15$. Reversing the monotone chain $i \mapsto 4-i$ turns an increasing nested flag into a decreasing one; complementing each mask restores an increasing flag. The module's deliverable on complement symmetry asserts that this operation sends Kuhn vertex-sets to Kuhn vertex-sets and swaps difference-mask types $(i,j)$ with $(j,i)$.
Local scope is pure combinatorics of hinges up to lattice translation and triangulation-preserving symmetry. No star kernels or Hessian entries are evaluated here.
proof idea
Finite exhaustion: case-split on the 24 values of $s$, then decide checks the existential witness $s'$ and the five pointwise mask equalities in each case. No algebraic lemma is invoked; the statement is a closed finite identity on the precomputed Kuhn table.
why it matters
This is item 4 of the module deliverable: complement symmetry of Kuhn vertex-sets. Together with the $S_4$ action on bit positions it generates the larger group $S_4 \rtimes {\mathrm{id},\mathrm{complement}}$, which merges hinge types $(1,2)\sim(2,1)$ and $(1,3)\sim(3,1)$ and yields four lattice orbits of triangle hinges.
That orbit count is the combinatorial prerequisite for assembling the flat 4D Regge Hessian from per-orbit star kernels (QG full-theory campaign). The module explicitly does not yet evaluate those kernels, complete the flat Hessian, prove $S_{\mathrm{RS}}\to S_{\mathrm{EH}}$ in 4D, or flip gap_action_recovery. No downstream theorem currently cites this lemma in the graph; it stands as a proved building block for the orbit-classification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.