vertexMask_end
plain-language theorem explainer
For every Freudenthal 4-simplex (one of the 24 axis permutations), the fifth nested vertex has bit-mask 15: the full opposite corner of the 4-cube. Anyone wiring hinge incidence or local edge masks in the 4D Regge flat-kernel skeleton cites this terminal identity. The proof is a one-line definitional equality.
Claim. For every simplex index $s\in\{0,\ldots,23\}$, the nested Freudenthal vertex mask after four axis steps equals $15$ (all four axis bits set).
background
In the Freudenthal/Kuhn subdivision of the unit 4-cube, each monotone 4-simplex is labeled by a permutation of the four coordinate axes. Nested vertices along a simplex are obtained by successively adjoining those axes: after $k$ steps the vertex is the bit-mask sum of the first $k$ axis masks, taking values in ${0,\ldots,15}$.
The module records that walk as a five-point mask function on each of the 24 simplices. Step 0 is the origin mask 0; intermediate steps accumulate the permuted axis bits (powers of two among ${1,2,4,8}$). The ambient cube vertices are exactly the subsets of the four axes.
Local setting is deliverable B of the Regge 4D flat-Hessian campaign: combinatorial incidence of the 15 edge classes on a seed hinge orbit, with per-hinge deficit and area kernels left OPEN parameters.
proof idea
One-line term proof by definitional equality (rfl). By construction the mask at step 4 is the sum of all four axis bit-masks of the permutation. Those masks are a rearrangement of ${1,2,4,8}$, so the sum is definitionally $15$.
why it matters
Fixes the terminal vertex of every Freudenthal 4-simplex used in the hinge-incidence bookkeeping. Sibling constructions (local edge pairs, local edge masks, edge-class membership of a simplex) read the five nested masks and need the walk to end at the opposite cube corner. The module header lists this among the proved combinatorial support items: 24 simplices, five nested vertices, ten edge-class masks, seed-hinge orbit, and incidence multiplicities.
No downstream theorem yet depends on it in the graph. It does not touch the OPEN per-hinge second-variation kernels, does not assemble the flat Hessian, and does not advance S_RS_converges_EH_4d or gap_action_recovery. Pure combinatorial gate for later MODEL assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.