orbitRep
plain-language theorem explainer
Canonical difference-mask pairs, one per S₄ lattice orbit type of triangle hinges in the 4D Kuhn cell. Each type (popcount pair) is represented by a fixed disjoint mask pair such as (1,2) for type (1,1). Downstream orbit-membership tests, covering permutations, and local star squares all pin against these six seeds. Pure pattern-match definition, no proof content.
Claim. For each of the six $S_4$ hinge-orbit types labeled by popcount pairs $(|a|,|b|)\in\{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)\}$, fix a canonical disjoint difference-mask representative: $(1,1)\mapsto(1,2)$, $(1,2)\mapsto(1,6)$, $(2,1)\mapsto(3,4)$, $(1,3)\mapsto(1,14)$, $(3,1)\mapsto(7,8)$, $(2,2)\mapsto(3,12)$.
background
In the 4D Kuhn triangulation of the unit hypercube, every oriented triangle hinge inside a simplex is a monotone vertex-mask chain $m_0\subset m_1\subset m_2$. Its geometry is encoded by the disjoint nonzero difference masks $(a,b)=(m_1\oplus m_0,,m_2\oplus m_1)$. The type of the hinge is the popcount pair $(|a|,|b|)$, which takes exactly six values: $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$.
The module classifies these hinges up to lattice translation and coordinate permutation $S_4$ acting on the four bit positions of the 4-cube. That action preserves type and is transitive on realizable pairs of each type, yielding six lattice orbits. The inductive type HingeOrbitType names those six orbits.
This definition supplies one concrete seed pair per orbit so that later constructions (orbit membership, covering permutations, local squared kernels) can be stated relative to a fixed representative rather than an arbitrary realizable pair.
proof idea
Definition by exhaustive pattern match on the six constructors of the orbit-type inductive. No lemmas, no tactics: each constructor is assigned a hard-coded natural-number pair that is known (and later proved by decide) to be realizable and to have the matching popcount type.
why it matters
This is the seed table for the entire orbit-transport layer of the 4D Regge flat-Hessian campaign. Membership tests ask whether a difference pair lies in the $S_4$-orbit of the representative; covering-permutation specs prove that a coordinate perm sends the representative onto any given slot of the same type; local star squares are evaluated once on the representative and then transported. Downstream consumers include the Bloch orbit-transport cover test and its packaging theorem, the in-orbit predicate, the per-orbit local square, and the two sanity theorems that the representatives are realizable and have the correct popcount type.
Within the module's stated scope this is pure combinatorics of triangle hinges in one unit 4-cube. It does not evaluate star kernels beyond the already-committed seed orbit, does not assemble the flat Hessian, and does not touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or gap-action recovery. It is the fixed reference frame that makes the six-orbit classification usable in later transport lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.