hingeVertexPermInv
plain-language theorem explainer
Lookup table giving, for each of the ten triangle-hinges of a 4-simplex, the inverse vertex permutation that pulls a local hinge labeling back to the seed simplex. Anyone assembling pathwise Schläfli summands or remapping squared-edge coordinates under hinge reindexing cites it. The body is an exhaustive case table on Fin 10 × Fin 5; no proof obligations.
Claim. For each hinge index $h \in \{0,\ldots,9\}$ and local vertex label $v \in \{0,\ldots,4\}$, the map returns the seed-simplex vertex corresponding to $v$ under the inverse of the hinge-$h$ vertex permutation. On the seed hinge $h=0$ the map is the identity; the remaining nine rows are fixed permutations of $\{0,1,2,3,4\}$.
background
The ambient module develops the Freudenthal/Kuhn 4-simplex analogue of the 3D Gate-A2 Schläfli input: ten edges and ten triangle-hinges ($n_H = n_E = 10$), flat hinge areas, a non-vacuous flat Schläfli identity witness, and directional kill of the Schläfli sum along every affine velocity through the flat seed.
A 4-simplex has five vertices. Each triangle-hinge is a 2-face; to write the Schläfli summand for that hinge one must reindex the five vertices so the hinge occupies a fixed local slot (the seed hinge). The forward map sends seed vertices to the local hinge frame; this definition is the inverse on vertices, so that lengths and areas computed in the seed frame can be pulled back under hinge reindexing.
Sibling combinatorics in the same file (local edge/hinge tables, flat squared-edge seeds, hinge boundary slots, flat hinge areas via Heron) supply the rest of the labeling data this inverse is meant to invert against.
proof idea
Pure definition by exhaustive pattern match: one clause per hinge index in Fin 10, and within each hinge a total map on Fin 5. Hinge 0 is the identity on vertices; hinges 1–9 are hard-coded permutations. No lemmas are invoked and there is no proof body.
why it matters
Pathwise Schläfli at the 4-simplex needs every hinge row written in a common seed edge basis. The inverse vertex permutation is the combinatorial glue that lets edge lengths feeding a remapped seed-slot be read off the global squared-edge vector, which is exactly the step the module tags as still open for full off-seed HasDerivAt on every hinge row.
It sits inside the THEOREM tier for Freudenthal 4-simplex hinge combinatorics and the flat Schläfli summand table, and supports the non-vacuous flat SchlaefliIdentityN witness at $n_H = n_E = 10$. It does not itself close the OPEN items (full pathwise identity off the flat seed, remapped derivatives for every hinge, elevation to the Regge candidate, or $S_{RS}\to$ Einstein–Hilbert in 4D), nor does it touch gap_action_recovery.
No downstream consumers are recorded yet in the graph; the declaration is infrastructure for those later hinge-row and assembly proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.