localEdge
plain-language theorem explainer
Local indexing of the ten edges of a 4-simplex: each slot in Fin 10 is sent to an unordered pair of vertices in Fin 5. Anyone assembling squared-edge coordinates, hinge boundaries, or flat Schläfli summands on the Freudenthal 4-simplex cites this map. The body is a pure alias of the upstream edge-pair table.
Claim. Define a local edge map $e\colon \{0,\ldots,9\}\to \{0,\ldots,4\}\times\{0,\ldots,4\}$ by identifying each of the ten edge slots of a 4-simplex with the corresponding ordered pair of its five vertices (the standard combinatorial edge table).
background
A 4-simplex has five vertices and therefore $\binom{5}{2}=10$ edges. In the Regge calculus setup of this module, squared edge lengths are coordinates on $\mathbb{R}^{10}$, and hinges (triangular faces) are assembled from those edges. The upstream definition localEdgePair fixes the concrete enumeration: slot 0 is vertices $(0,1)$, slot 1 is $(0,2)$, and so on through all ten pairs.
This module mirrors the 3D Gate-A2 Schläfli input (six edges on a tetrahedron) at the 4-simplex level with $n_H=n_E=10$. The local edge map is the shared combinatorial skeleton for flat hinge areas, the flat Schläfli summand table, and directional derivatives of dihedral angles through the flat seed.
proof idea
One-line definitional alias: localEdge is definitionally equal to the upstream localEdgePair table. No proof obligations; the Fin 10 cases are already discharged in the imported kernel module.
why it matters
Gives this module a short local name for the ten edge slots without re-importing the full flat-kernel namespace at every use site. It underpins the THEOREM-tier claims listed in the module doc: Freudenthal/Kuhn 4-simplex edge and triangle-hinge combinatorics, flat hinge areas, the flat Schläfli summand table, and the non-vacuous flat SchlaefliIdentityN witness at $n_H=n_E=10$. Downstream open work (full pathwise identity off the flat seed, remapped HasDerivAt for every hinge row, elevation to the Regge candidate, and $S_{RS}\to$ Einstein–Hilbert in 4D) all sit on the same edge indexing. No used_by edges are recorded yet; the alias is scaffolding for those pathwise arguments rather than a cited lemma itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.