remappedSqEdges
plain-language theorem explainer
Remaps a 4-simplex squared-edge assignment so a chosen triangle hinge sits in the Gram seed slots (0,1,2). Anyone reducing an arbitrary hinge row to the seed-hinge dihedral kernel cites this pullback. The body is the pure composition a ∘ pullEdgeSlot h.
Claim. Given a hinge index $h \in \{0,\ldots,9\}$ and a squared-edge map $a:\{0,\ldots,9\}\to\mathbb{R}$, define the remapped assignment by $(a\circ\pi_h)(e)=a(\pi_h(e))$, where $\pi_h$ is the combinatorial edge-slot pull that places hinge $h$ into the seed slots $(0,1,2)$.
background
The module develops pathwise Schläfli identities for the Freudenthal (Kuhn) 4-simplex, the 4D analogue of the closed-form six-edge tetrahedron identity. A 4-simplex has ten edges and ten triangle hinges; squared lengths live in SqEdges4 ≅ Fin 10 → ℝ, ordered by the local incidence layer.
Seed analysis is fixed at hinge 0 with Gram slots (0,1,2). To reuse the seed dihedral kernel and flat Hessian on every hinge, edge coordinates must be pulled so that hinge h occupies those slots. The companion map pullEdgeSlot h supplies the Fin 10 → Fin 10 permutation (identity on hinge 0; explicit tables for hinges 1 and 2, and by extension the rest).
This sits under the binding tier that already proves flat hinge areas, vanishing column sums, and seed-hinge HasDerivAt along squared-edge paths; full off-seed pathwise identity remains open.
proof idea
One-line definitional wrapper: evaluate the input squared-edge map at the pulled slot, fun e => a (pullEdgeSlot h e). No lemmas; pure function composition with the combinatorial pullback.
why it matters
Enables hinge-uniform statements from seed-only analysis. Downstream, remappedSqEdges_zero and remappedSqEdges_seed_id show hinge 0 is the identity on every assignment and on the flat seed; remapped_seed_dihedral_eq then transfers the seed dihedral angle unchanged under the h=0 remap.
That transfer is the bridge from the proved seed-hinge row (matching hingeArea · angleKernel) toward remapped HasDerivAt for every hinge row and the still-open full pathwise Schläfli identity on Nondeg4Simplex. It is scaffolding for Gate-A2-style flat directional kill at nH = nE = 10, not a claim about continuum Einstein–Hilbert recovery or gap-action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.