pullEdgeSlot
plain-language theorem explainer
Lookup table that, for each of the ten triangle-hinges of a 4-simplex, renumbers the ten edge slots so that hinge sits in the Gram seed positions (0,1,2). Anyone assembling pathwise Schläfli or remapped squared-edge data cites it. The body is a pure Fin 10 × Fin 10 case table; no proof obligations.
Claim. A function $\mathrm{pull}:\{0,\ldots,9\}\times\{0,\ldots,9\}\to\{0,\ldots,9\}$ such that, for hinge index $h$ and seed edge index $e$, $\mathrm{pull}(h,e)$ is the edge whose squared length is written into seed slot $e$ when hinge $h$ is moved to the Gram seed face with vertices $(0,1,2)$. On $h=0$ it is the identity.
background
The module develops Freudenthal/Kuhn 4-simplex Schläfli identities pathwise, mirroring the 3D Gate-A2 closed form (six edges, six hinges) at $n_H=n_E=10$. Squared edge lengths live in a 10-slot array; dihedral and area kernels are tabulated at a fixed flat seed whose distinguished hinge occupies slots $(0,1,2)$.
To reuse that seed kernel on an arbitrary hinge, one must pull the three edges of the target hinge (and the remaining seven edges consistently) into the seed numbering. This definition is that combinatorial pull map. Upstream hinge combinatorics (shared triangle faces of glued simplices) fix which three edges belong to each hinge; the table encodes the full edge permutation that realizes the move.
Sibling objects include the squared-edge type, local edge/hinge indexers, and flat seed edge data against which the $h=0$ row is checked.
proof idea
No proof: it is a definition by exhaustive pattern match on the pair $(h,e)\in\mathrm{Fin},10\times\mathrm{Fin},10$. The $h=0$ row is the identity map on edge slots. Each other row is a fixed permutation of ${0,\ldots,9}$ sending the three edges of hinge $h$ to seed slots $0,1,2$ and completing the remaining seven slots by the Freudenthal edge labeling convention used elsewhere in the module.
why it matters
Parent consumers are the remapped squared-edge map (compose the array with this pull), the identity check that hinge $0$ leaves the flat seed fixed, and the theorem that remapping under hinge $0$ is the identity on every squared-edge array. Those feed the pathwise flat directional Schläfli kill and the seed-hinge $\mathrm{HasDerivAt}$ statements listed as THEOREM tier in the module doc.
In the Recognition gravity stack this is scaffolding for Gate-A2-style input at four dimensions: without a hinge-to-seed edge renumbering one cannot recycle the flat dihedral kernel across all ten hinges. It does not close the OPEN items (full pathwise identity off the flat seed, remapped derivatives for every hinge row, elevation to the continuum candidate, or $S_{RS}\to EH$ in 4D), and it does not touch gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.