localEdgePair
plain-language theorem explainer
Enumerates the ten unordered edge slots of a 4-simplex as ordered pairs among five local vertices (0..4). Anyone assembling Freudenthal hinge incidence, local edge masks, or squared-length vectors in the 4D Regge kernel cites this table. The body is a pure pattern-match lookup with an absurdity branch for out-of-range indices.
Claim. The map $e \mapsto (i,j)$ sends each local edge index $e \in \{0,\ldots,9\}$ to one of the ten ordered pairs of distinct vertices among five labeled vertices of a 4-simplex, in the fixed order $(0,1),(0,2),(0,3),(0,4),(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)$.
background
This module builds the combinatorial support for the flat Hessian of the 4D Regge action on a Freudenthal (Kuhn) triangulation of the 4-cube. A 4-simplex has five vertices and therefore $\binom{5}{2}=10$ edges. The fifteen global edge classes of the imported 4D edge stencil are never redefined here; local slots are only a labeling inside one simplex.
Upstream, a single abstract edge is the two-vertex complex with one joining edge. Here that idea is specialized to an explicit bijection from Fin 10 onto the ten pairs among five local vertex labels. Downstream masks XOR the two vertex bitmasks of a pair, so the pair table is the sole source of which vertices an edge joins.
The module scope is deliberately narrow: incidence multiplicities and an assembly skeleton that contracts open per-hinge area and deficit kernels. It does not evaluate those kernels or claim Einstein–Hilbert recovery.
proof idea
Definition by exhaustive pattern match on the ten inhabitants of Fin 10. Each clause returns a fixed ordered pair of Fin 5 indices. The residual constructor ⟨n+10, h⟩ is discharged by absurd plus omega, since no such proof of membership in Fin 10 exists. No lemmas are invoked.
why it matters
This table is the shared local edge ordering for the hinge-incidence layer. Downstream, pathwise Schläfli code aliases it as the local edge map; the dihedral kernel packages squared lengths as a ten-component vector in exactly this slot order; and the flat-kernel mask of edge $e$ in simplex $s$ is the XOR of the two vertex masks of the pair returned here.
In the QG campaign this is deliverable-B scaffolding: combinatorial support for seed-hinge orbits and the fifteen-class incidence counts (three decoys, three hinge-boundary classes of multiplicity two). It does not close the open per-hinge flat second-variation kernels, nor flip action-recovery or EH-convergence goals. It only fixes the edge-slot convention those later kernels must respect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.