hingeVertexPerm
plain-language theorem explainer
Explicit vertex permutations of the 4-simplex that send each of the ten triangle hinges to the seed hinge (0,1,2). Gravity analysts cite it when reducing hinge-row Schläfli summands and Gram data to the seed table. The body is a pure case table on Fin 10 × Fin 5; no proof obligations.
Claim. A map $\sigma:\{0,\ldots,9\}\to\mathrm{Sym}(\{0,1,2,3,4\})$ such that, for each hinge index $h$, the permutation $\sigma_h$ carries hinge $h$ onto the seed hinge $(0,1,2)$. Values are given by an explicit lookup table (identity on $h=0$).
background
The ambient module treats the Freudenthal/Kuhn 4-simplex at the Regge level: ten edges and ten triangle hinges ($n_H=n_E=10$), mirroring the 3D Gate-A2 closed-form Schläfli input. A hinge is a triangular face shared by two tetrahedra inside the 4-simplex; the seed hinge is the ordered triple of vertices $(0,1,2)$.
Pathwise Schläfli identities and flat directional kills are first proved on the seed row, then transported to the other nine hinges by vertex relabeling. The present map supplies those relabelings. Remapped Gram cosines and flat Jacobians are required to match the summand table; that match is numerically checked, with a Lean geometric proof still open for $h\neq 0$.
Related local data include squared-edge coordinates, flat hinge areas, and the dihedral angle kernel from the hinge-4D modules imported here.
proof idea
Definition by exhaustive pattern match: ten clauses, one per hinge index in Fin 10, each assigning an image in Fin 5 to every vertex. Clause 0 is the identity. No lemmas, tactics, or obligations; the table is the content.
why it matters
Sits in the THEOREM tier of the Freudenthal 4-simplex pathwise Schläfli program: combinatorics, flat hinge areas, the flat summand table, and seed-row agreement with hingeArea · angleKernel. Without a uniform vertex transport, only the seed hinge would be under Lean control.
It is the combinatorial substrate for the still-OPEN items listed in the module doc: remapped HasDerivAt on every hinge row, full pathwise identity off the flat seed on nondegenerate 4-simplices, elevation to a Regge candidate, and $S_{RS}\to$ Einstein–Hilbert in 4D. It does not touch gap-action recovery or the vacuous-shell lesson.
In the broader RS gravity stack this is infrastructure for discrete curvature identities that feed continuum recovery, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.