cornerContainsMask
plain-language theorem explainer
Boolean predicate: absolute vertex mask m sits inside the axis-aligned unit cube whose corner is the 4-bit code c. Used when enumerating which of the 16 corners of the Freudenthal lattice contain the type-(2,2) hinge. Implemented by a decidable bit test: every axis where c is shifted to −1 must have m’s corresponding bit clear.
Claim. Given a cube corner $c\in\{0,\ldots,15\}$ (bit $i$ set means the cube is shifted to coordinate $-1$ on axis $i$) and an absolute vertex mask $m\in\mathbb{N}$, return true if and only if for every axis $i\in\{0,1,2,3\}$, either bit $i$ of $c$ is unset or bit $i$ of $m$ is unset. Equivalently: on every negatively shifted axis the absolute coordinate of $m$ is $0$.
background
This module builds the full periodic-lattice star deficit kernel for the type-(2,2) triangle hinge in 4D Regge calculus (masks ${0,3,15}$, difference masks $(3,12)$). The campaign enumerates every (cube translate, Kuhn simplex) pair that contains the hinge and checks flat cosine and angle-sum gates.
A cube corner is encoded as a 4-bit mask in $\mathrm{Fin},16$: bit $i$ set means the unit cube has lower corner coordinate $-1$ on axis $i$, otherwise $0$. Absolute vertex masks are ordinary natural numbers whose bits mark occupied axes. Geometric containment of a vertex in such a shifted unit cube reduces to a pure bit condition: wherever the cube is shifted negative, the vertex must sit at absolute coordinate $0$ on that axis.
The predicate is the atomic containment test used by the star-enumeration layer; it does not itself mention hinges or simplices.
proof idea
Definition, not a theorem. The body is a single decide of the universal quantifier over the four axes: for each $i:\mathrm{Fin},4$, either bit $i$ of the corner code is clear or bit $i$ of the absolute mask is clear (Nat.testBit). Lean’s decidable instance for Boolean combinations of bit tests discharges the Bool return type. No lemmas are applied.
why it matters
Feeds directly into cornerContainsHinge, which asks whether every absolute hinge mask lies in the given corner cube. That hinge-level check is the filter used to prove deliverable A.1 of the module: among all 16 axis-aligned unit-cube corners with coordinates in ${-1,0}$, only the origin corner contains the absolute (2,2) hinge, and exactly four (cube translate, Kuhn simplex) pairs make up the full periodic Freudenthal star.
The star enumeration is a prerequisite for the flat cosine multiset, the $2\pi$ angle-sum flatness gate, and the closed-form full-star deficit class kernel on the 15 stencil classes. The module explicitly does not complete flat Hessian assembly, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and does not flip gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.