triangle_diff_masks_ok
plain-language theorem explainer
Every triangle slot in the 24-simplex Kuhn cell has difference masks that are nonzero, bitwise disjoint, and each at most 15 (four bits). Combinatorialists building Regge flat Hessians from per-orbit star kernels cite this as basic well-formedness of the (a,b) type data. The proof is exhaustive finite case analysis over all 240 slots.
Claim. For every Kuhn simplex index $s\in\{0,\ldots,23\}$ and every triangle slot $t\in\{0,\ldots,9\}$, writing $a=m_1\oplus m_0$ and $b=m_2\oplus m_1$ for the successive XOR differences of the vertex-mask chain of that slot, one has $a>0$, $b>0$, $a\land b=0$, and $a\le 15$, $b\le 15$.
background
This module classifies triangle hinges in one unit 4-cube under the Freudenthal/Kuhn triangulation. There are 24 oriented Kuhn simplices and $\binom{5}{3}=10$ index-triple triangle slots per simplex, hence 240 oriented slots in the cell. Each slot carries three vertex masks forming a monotone chain $m_0\subset m_1\subset m_2$ inside the 4-bit cube ${0,\ldots,15}$.
The first and second difference masks are the successive XORs $a=m_1\oplus m_0$ and $b=m_2\oplus m_1$. Their popcount pair $(|a|,|b|)$ is the combinatorial type of the hinge; the module later shows the only realizable types are ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. The present statement is the elementary well-formedness of $(a,b)$: nonzero, disjoint, and supported on four bits.
The local setting is combinatorics only of triangle hinges up to lattice translation and triangulation-preserving symmetry. It imports the 24-simplex/vertexMask API and the 15-class mask utilities; it does not evaluate star kernels or assemble the flat Hessian.
proof idea
Term-mode proof by exhaustive enumeration. fin_cases s splits on the 24 simplex indices; nested fin_cases t splits on the 10 triangle slots; each of the 240 residual goals is closed by decide, which evaluates the concrete natural-number expressions for the two difference masks and checks positivity, bitwise disjointness, and the bound $\le 15$. No intermediate lemmas are required beyond the definitions of the two difference masks via XOR of the triangle vertex-mask triple.
why it matters
This is the first deliverable of the Regge 4D triangle-hinge orbit classification: every index-triple triangle is a genuine monotone mask chain with disjoint nonzero difference masks. All later counts (per-type tallies $(72,48,48,24,24,24)$, $S_4$ orbit transitivity, complement symmetry merging six popcount types into four lattice orbits) rest on $(a,b)$ being well-formed bitmasks in ${1,\ldots,15}$.
In the QG full-theory campaign this is a combinatorial prerequisite for assembling the flat Hessian from per-orbit star kernels. It does not itself evaluate those kernels or prove continuum recovery of the Einstein-Hilbert action; it only certifies that the type data fed into those constructions is legitimate. No downstream theorem currently depends on it in the graph, but sibling orbit-type maps and per-type counters are the immediate consumers inside the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.