hingeBase
plain-language theorem explainer
Base vertex of a triangle hinge inside one Kuhn 4-simplex, returned as a {0,1}^4 coordinate covector. Gravity analysts cite it as the origin for every midpoint plane-wave phase and exact flat cross-term on that hinge. One-line extraction: first ordered vertex mask of the slot, bit-decoded to coordinates.
Claim. For each oriented Kuhn 4-simplex $s\in\{0,\ldots,23\}$ and triangle slot $t\in\{0,\ldots,9\}$, the hinge base is the map $\mathrm{Fin}\,4\to\mathbb{R}$ sending coordinate $i$ to $1$ if bit $i$ of the first ordered vertex mask of $(s,t)$ is set, and to $0$ otherwise.
background
The module runs the QG full-theory campaign for the exact phase-decorated Bloch fold of the committed true-weight flat Hessian on type-(1,1) triangle hinges in one Kuhn cell. Scope is the (1,1) orbit only (72 oriented slots per cell), using the midpoint plane-wave convention of the edge stencil.
Vertex masks encode the four corners of a Kuhn simplex as bit-patterns in $\mathbb{N}$. The ordered triple of vertex masks for triangle slot $t$ in simplex $s$ is produced by triangleVertexMasks; its first component is the geometric base vertex of that hinge. maskCoord turns a mask into a coordinate function on $\mathrm{Fin},4$ by reading bits: set bit $\mapsto 1$, unset $\mapsto 0$.
Together these give a concrete ${0,1}^4$ position that every phased class-dot and deficit contraction treats as the hinge origin under the midpoint convention.
proof idea
Pure definitional composition: apply the bit-decoder to the first component of the ordered vertex-mask triple of $(s,t)$. No proof obligations.
why it matters
Every finite-momentum slot term in the 4D Regge Bloch analysis needs a geometric origin for the midpoint phase. This base feeds the exact deficit side and the exact flat cross-term slot in the exact-action symbol module, the factorized orbit slot term and its $m^2$ moment polynomial in the all-orbit symbol module, and the local (1,1) bilinear Bloch fold and its scalar-multiplication lemmas in this module.
It is infrastructure for the closed geometric-certificate match at the star wavevector (axis table sum $-3$, gauge table $-4+4\sqrt{2}$) and for the nonvacuity of the transported fold. It does not itself touch continuum EH recovery or the open Tendsto glue on the $m^2$ coefficient; those sit downstream of the folds that consume this base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.