localHinge
plain-language theorem explainer
Local alias for the ten triangle-hinge labels of a 4-simplex: each hinge index in Fin 10 maps to an increasing triple of vertices in Fin 5. Gravity analysts cite it when wiring flat Schläfli summands and seed-hinge identities to concrete vertex combinatorics. The body is a pure abbreviation of the orbit-classification table triangleIndexTriple.
Claim. Define a local hinge map $\mathrm{localHinge}:\{0,\ldots,9\}\to\{0,\ldots,4\}^3$ by the standard enumeration of the $\binom{5}{3}=10$ increasing vertex triples of a 4-simplex (identical to the orbit-classification table of triangle index triples).
background
The module develops pathwise Schläfli identities for the Freudenthal/Kuhn 4-simplex at $n_H=n_E=10$, mirroring the 3D Gate-A2 closed form for the tetrahedron ($n_H=n_E=6$). Hinges of a 4-simplex are its triangular 2-faces; each contributes an area–dihedral summand to the discrete Schläfli relation used in Regge calculus.
Upstream, triangleIndexTriple is the fixed combinatorial table of all $C(5,3)=10$ increasing vertex-index triples in a 4-simplex, beginning $(0,1,2)$, $(0,1,3)$, $(0,1,4)$, and so on. Squared edge lengths live on Fin 10; hinge rows are likewise indexed by Fin 10. Naming that table locally keeps hinge-row proofs readable beside edge and area kernels imported from the Regge hinge modules.
The flat seed and directional Schläfli kill theorems in this file evaluate summands hinge-by-hinge against that enumeration, so a stable local name for the triple map is part of the bookkeeping layer rather than a new geometric claim.
proof idea
One-line definitional alias: localHinge is definitionally equal to triangleIndexTriple. No tactics, no lemmas, no computation beyond the upstream case table on Fin 10.
why it matters
Feeds the seed-hinge bookkeeping theorem seed_hinge_is_zero, which records that hinge 0 is the face $(0,1,2)$ by rfl. That fact sits under the flat closed-form column-sum theorems (freudenthal4SimplexFlatSchlaefli and its real variant): vanishing of $\sum_h$ flat Schläfli summands at every edge coordinate uses the same hinge indexing.
In the module tier list this supports THEOREM-tagged flat hinge areas, the flat summand table, and the non-vacuous flat SchlaefliIdentityN witness at $n_H=n_E=10$. It does not touch the OPEN pathwise identity off the flat seed, elevation to the RS candidate, or $S_{RS}\to$ EH in 4D. Within Recognition gravity it is pure combinatorics scaffolding for discrete curvature identities that later interface with continuum limits; it does not itself invoke $\phi$, the eight-tick octave, or the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.