isRealizableDiffPair
plain-language theorem explainer
Boolean predicate: a pair of naturals (a,b) is a realizable difference pair iff it equals the successive XOR masks of some oriented triangle in a Kuhn 4-simplex of the unit cube. Orbit-classification and Hessian-assembly arguments cite it to separate genuine hinge types from decoys. The body is a decidable existential over the 24 simplices and 10 triangle slots.
Claim. For $a,b\in\mathbb{N}$, return true iff there exist a Kuhn simplex $s\in\{0,\ldots,23\}$ and triangle slot $t\in\{0,\ldots,9\}$ such that the first difference mask of that slot equals $a$ and the second equals $b$.
background
The module classifies triangle hinges in one unit 4-cube Kuhn triangulation, up to lattice translation (difference masks) and triangulation-preserving symmetry. It is a combinatorial prerequisite for assembling the flat Hessian of the 4D Regge action from per-orbit star kernels; it does not evaluate those kernels or close the Einstein-Hilbert recovery gap.
Each oriented triangle in a Kuhn simplex is a monotone vertex-mask chain $m_0\subset m_1\subset m_2$. The successive XOR differences $a=m_1\oplus m_0$ and $b=m_2\oplus m_1$ are the difference masks. Upstream, diffMaskA and diffMaskB extract those two masks from the triangle-vertex-mask triple of simplex $s$ and slot $t$. Realizable pairs are exactly those that arise this way; their popcount types lie in ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$.
proof idea
Definition, not a theorem. The body is a single decide on the proposition that there exist $s:\mathrm{Fin},24$ and $t:\mathrm{Fin},10$ with diffMaskA s t = a and diffMaskB s t = b. Lean discharges the finite search automatically; no manual case split is written here.
why it matters
This predicate is the gate used by the module's realizability theorems. disjoint_implies_realizable shows every bitwise-disjoint nonzero 4-bit pair is realized; decoy_overlapping_not_realizable shows the overlapping decoy $(1,3)$ is not; orbitRep_realizable certifies that each orbit representative is realized. Together they underwrite deliverable A of the module: six $S_4$ orbits of difference pairs (four under the larger group with complement), which is the combinatorial skeleton needed before per-orbit star kernels can be summed into the flat Hessian. It does not itself touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or the action-recovery gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.