triangleTypeNat
plain-language theorem explainer
Indicator returning 1 when an oriented triangle slot in the unit 4-cube Kuhn triangulation has a prescribed difference-mask popcount pair, else 0. Cell-wide type enumerations sum this over the 24 simplices and 10 triangle slots. The body is a one-line equality test against the slot's popcount pair.
Claim. For simplex index $s\in\{0,\ldots,23\}$, oriented triangle index $t\in\{0,\ldots,9\}$, and pair $p\in\mathbb{N}\times\mathbb{N}$, define the indicator $I_{s,t}(p)=1$ if the difference-mask popcount pair of slot $(s,t)$ equals $p$, and $I_{s,t}(p)=0$ otherwise.
background
The module classifies triangle hinges in one unit 4-cube under the Freudenthal/Kuhn triangulation: 24 oriented 4-simplices, each with $C(5,3)=10$ oriented triangle faces, hence 240 slots. Scope is pure combinatorics of difference masks up to lattice translation and triangulation-preserving symmetry; it does not evaluate star kernels or the flat Hessian.
Each slot carries two disjoint nonzero difference masks $(a,b)$ along a monotone vertex-mask chain. The popcount pair $(|a|,|b|)$ is the type, restricted to the six realizable values ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. The upstream map that extracts this pair from $(s,t)$ is the slot popcount-type function built from the two difference-mask popcounts.
This indicator is the standard 0-1 test of that pair against a target $p$, so that summing it over all slots yields the cell-wide multiplicity of each type.
proof idea
Definition, not a proof. Body is a single conditional: compare the slot's popcount pair to the target $p$ and return $1$ on equality, else $0$. No lemmas are invoked.
why it matters
This is the summand for the cell-wide type counter, which totals oriented triangle slots of a fixed popcount pair over all $24\times 10$ slots. Downstream, that counter is unfolded in the orbit-slot-count identity equating summed orbit indicators to the committed per-orbit cell counts, and in the private $(1,1)$-count lemma that recovers the multiplicity 72.
In the QG campaign this sits in deliverable A of the hinge-orbit classification: the combinatorial prerequisite for assembling the flat Hessian from per-orbit star kernels. It does not itself close Hessian assembly, action recovery, or convergence of the RS action to Einstein-Hilbert in 4D; it only supplies the 0-1 brick those enumerations rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.