complement_swaps_diff_pair
plain-language theorem explainer
For every oriented triangle slot in the 24 Kuhn simplices, there is another slot whose difference-mask pair is exactly the swap (b,a) of the original (a,b). Orbit classifiers cite this to identify the complement symmetry that merges types (i,j) with (j,i). The proof is exhaustive finite case analysis over Fin 24 × Fin 10.
Claim. For every Kuhn simplex index $s \in \{0,\ldots,23\}$ and every triangle-slot index $t \in \{0,\ldots,9\}$, there exist $s',t'$ such that the first difference mask of $(s',t')$ equals the second difference mask of $(s,t)$, and the second difference mask of $(s',t')$ equals the first difference mask of $(s,t)$. Equivalently, complement (after reversing the monotone chain) sends the pair $(a,b)$ to $(b,a)$ on the nose.
background
This module classifies triangle hinges in one unit 4-cube Kuhn triangulation, up to lattice translation and triangulation-preserving symmetry. It is a combinatorial prerequisite for assembling the flat Hessian of the 4D Regge action from per-orbit star kernels. Scope is combinatorics only: no star-kernel evaluation and no claim that the RS action converges to Einstein–Hilbert.
Each oriented triangle in a Kuhn simplex is a monotone vertex-mask chain $m_0 \subset m_1 \subset m_2$. The two nonzero disjoint difference masks are $a = m_1 \oplus m_0$ and $b = m_2 \oplus m_1$, exposed here as diffMaskA and diffMaskB. The popcount pair $(|a|,|b|)$ is the hinge type, taking values in ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. There are $24 \cdot C(5,3) = 240$ oriented triangle slots.
Bitwise complement $m \mapsto m \oplus 15$ preserves Kuhn vertex-sets. The module claims that under the larger group $S_4 \rtimes {\mathrm{id},\mathrm{complement}}$, types $(i,j)$ and $(j,i)$ merge, cutting six $S_4$-orbits down to four lattice orbits. This theorem is the mask-level swap that underlies that type interchange.
proof idea
Term-mode proof by exhaustive enumeration. Both parameters are finite: $s : \mathrm{Fin},24$ indexes Kuhn simplices and $t : \mathrm{Fin},10$ indexes the $C(5,3)$ triangle slots inside a 5-vertex simplex. The tactic fin_cases s <;> fin_cases t <;> decide splits into all $240$ concrete pairs and discharges each goal by kernel decision procedure on the concrete natural-number equalities of the two XOR masks. No intermediate lemmas are invoked beyond the definitions of the two difference masks.
why it matters
Deliverable A of the module lists complement symmetry as item 4: bitwise complement sends Kuhn vertex-sets to themselves and swaps type $(i,j)$ with $(j,i)$, so under $S_4 \rtimes {\mathrm{id},\mathrm{complement}}$ one obtains four lattice orbits rather than six. This theorem is the concrete mask identity $(a,b)\mapsto(b,a)$ that makes that type swap hold on the nose for complementary-nested chains.
No downstream consumers are wired yet in the graph (used_by is empty). The intended landing zone is the orbit-classification pipeline that feeds per-orbit star kernels and, later, the flat Hessian of the 4D Regge action. The module explicitly does not yet prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, nor does it flip gap_action_recovery; this lemma only closes the combinatorial complement half of the orbit count.
In the broader Recognition gravity campaign, correct hinge-orbit counts are a prerequisite before any continuum or curvature identification is attempted. The result is pure finite combinatorics inside one unit 4-cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.