hingeBoundarySlots
plain-language theorem explainer
Lookup table assigning, to each of the ten triangle-hinges of a Freudenthal 4-simplex, the three global edge indices that bound that hinge, ordered as opposite-vertex pairs (v0v1, v0v2, v1v2). Anyone computing flat hinge areas or assembling the 4D Schläfli summand table cites it. The body is a pure case table on Fin 10 × Fin 3.
Claim. For each hinge index $h \in \{0,\ldots,9\}$ and each local boundary slot $s \in \{0,1,2\}$, the map returns the global edge index in $\{0,\ldots,9\}$ of the $s$-th edge of hinge $h$, ordered as the three edges $(v_0v_1,\, v_0v_2,\, v_1v_2)$ of the triangular face dual to that hinge. The default branch returns $0$.
background
The module lifts the 3D Gate-A2 Schläfli input (six edges, six hinges on a tetrahedron) to the Freudenthal/Kuhn 4-simplex, which has ten edges and ten triangle-hinges. In Regge calculus the curvature lives on hinges; each hinge is a triangle whose three boundary edges are a subset of the ten squared-edge coordinates.
Squared edge lengths are indexed by Fin 10. A hinge is likewise indexed by Fin 10. To evaluate the area of hinge $h$ via Heron's formula one must pull the three relevant squared lengths out of the global edge vector. This definition is exactly that pullback: slot $0$ is edge $v_0v_1$, slot $1$ is $v_0v_2$, slot $2$ is $v_1v_2$.
Sibling combinatorics (localEdge, localHinge, flatSqEdges) fix the same Freudenthal labeling used by the dihedral-kernel and Hessian-assembly modules imported here.
proof idea
Pure definition by exhaustive pattern match on the pair $(h,s) \in \mathrm{Fin},10 \times \mathrm{Fin},3$. Each of the ten hinges is given an explicit triple of edge indices; the catch-all branch returns $0$ and is unreachable on the stated domain. No lemmas are invoked.
why it matters
Every flat hinge-area evaluation in the module (hingeAreaFlat_0 through hingeAreaFlat_7 and the remaining rows) unfolds this table, then feeds the three squared lengths into Heron. Those areas are the coefficients in the flat Schläfli summand table whose column sums vanish, supplying the non-vacuous flat SchlaefliIdentityN witness at $n_H = n_E = 10$ required by the module's THEOREM tier.
Downstream the same indexing supports seed-hinge directional derivatives and the flat directional Schläfli kill (Gate A2-style input at flat). It does not yet close the OPEN items: full pathwise identity off the flat seed, remapped HasDerivAt for every hinge row, or elevation to the Einstein-Hilbert candidate. Framework landmark: discrete 4D Regge geometry underlying the continuum limit toward $D=3$ spatial plus time, not a forcing-chain (T0-T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.