isDisjointDiffPair
plain-language theorem explainer
A Boolean predicate on two natural numbers that is true exactly when both are nonzero 4-bit masks in {1,…,15} and their bitwise AND vanishes. Orbit-classification and hinge-type arguments in the 4D Kuhn/Regge combinatorics cite it to filter admissible difference-mask pairs. The body is a single `decide` on five arithmetic/bitwise constraints.
Claim. For $a,b\in\mathbb{N}$, return true if and only if $0<a$, $0<b$, $a\le 15$, $b\le 15$, and $a\land b=0$ (bitwise AND). Equivalently: $a$ and $b$ are nonzero masks in $\{1,\ldots,15\}$ that are bitwise disjoint.
background
The ambient module classifies triangle hinges in one unit 4-cube Kuhn triangulation, up to lattice translation (difference masks) and triangulation-preserving symmetry. Every index-triple triangle in a Kuhn simplex is a monotone mask chain $m_0\subset m_1\subset m_2$ whose successive differences $(a,b)=(m_1\oplus m_0,,m_2\oplus m_1)$ are nonzero and bitwise disjoint; the hinge type is the popcount pair $(|a|,|b|)$.
Masks live in the 4-bit range ${0,\ldots,15}$ (vertex labels of the Freudenthal/Kuhn cell). The predicate packages the combinatorial filter "nonzero, in-range, and land-zero" used throughout the difference-mask type and lattice-orbit arguments. Upstream bit maps Booleans to ${0,1}$ for mask construction; the module imports the 24 Kuhn simplices and 15-class mask utilities without redefining them.
proof idea
Definitional, not a proof. The body is one decide on the conjunction $0<a\land 0<b\land a\le 15\land b\le 15\land\mathrm{Nat.land},a,b=0$. Lean reduces the Boolean by decidable arithmetic and bitwise equality; no lemmas are invoked.
why it matters
Delivers the atomic filter for admissible difference-mask pairs in deliverable A of the Regge 4D hinge orbit classification: every realizable disjoint pair appears, $S_4$ acts transitively on each popcount type, and complement merges $(i,j)$ with $(j,i)$ into four lattice orbits. Downstream, decoy_overlapping_is_not_disjoint uses it to certify that the overlapping pair $(1,3)$ fails the filter (isDisjointDiffPair 1 3 = false), anchoring seed-hinge and decoy checks.
Combinatorial prerequisite only: it does not evaluate star kernels, assemble the flat Hessian, or touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ / gap_action_recovery. It sits in the QG full-theory campaign's hinge bookkeeping before continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.