localHingeMasks
plain-language theorem explainer
The type-(1,3) triangle hinge in the origin unit cube is fixed by the three absolute vertex masks {0, 1, 15}. Star-deficit and incidence proofs for the (1,3) Regge kernel cite this set as the local hinge data. It is a literal three-element Finset constant matching the module's absolute-mask convention.
Claim. The local absolute masks of the type-$(1,3)$ triangle hinge inside the origin cube are the finite set $\{0, 1, 15\}$.
background
This module is the QG full-theory kernel for the Regge 4D type-(1,3) periodic-lattice star deficit, after the type-(1,1) seed orbit and the orbit-classification layer. Vertices of the unit 4-cube are labeled by bitmasks in ${0,\ldots,15}$. A triangle hinge is specified by three absolute masks; here the type-(1,3) hinge is ${0, e_0, e_0+e_1+e_2+e_3}={0,1,15}$, with difference masks $(1,14)$ and flat squared edge lengths $(1,3,4)$.
Sibling kernels use the same name for different hinge types: type (1,1) spreads masks over several cube translates, type (1,2) uses ${0,1,7}$ at the origin, and type (2,2) images absolute masks through a local-mask map. This definition is the origin-only, type-(1,3) instance. Incidence is checked by asking whether every mask in the set appears among a Kuhn simplex's five vertex masks.
proof idea
Pure definition: the Finset literal ${0,1,15}$. No lemmas, tactics, or computation. The value is the absolute-mask triple fixed by the module scope for the type-(1,3) hinge in the origin cube.
why it matters
This constant is the incidence seed for the type-(1,3) star. Downstream, containsHinge decides membership by requiring every mask in the set to appear as a vertex mask of a Kuhn simplex (Fin 24). That predicate drives star enumeration: exactly six origin-cube simplices contain the hinge, and among translates in ${-1,0,1}^4$ only the origin does.
Those six simplices share flat cosine $1/2$, so the star angle sum is $2\pi$ and the deficit vanishes at flatness. The same incidence data feeds the ten coordinate derivatives and the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$. Transport to the complementary type $(3,1)$ remains open; this definition does not close that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.