remappedSqEdges_zero
plain-language theorem explainer
Remapping the ten squared edge lengths of a Freudenthal 4-simplex so that hinge 0 sits in the Gram seed slots is the identity on edge data. Anyone proving that the seed dihedral angle is unchanged under the zero remapping cites this. The argument is function extensionality plus the pull-slot table, which is the identity on hinge 0.
Claim. Let $a:\{0,\ldots,9\}\to\mathbb{R}$ be any assignment of squared edge lengths on the ten edges of a 4-simplex. The edge remapping that places hinge $0$ into the Gram seed slots leaves $a$ fixed: $\mathrm{remap}_0(a)=a$.
background
This module develops the pathwise Schläfli identity for the Freudenthal (Kuhn) 4-simplex, the 4D analogue of the closed-form six-edge tetrahedron identity. Combinatorics run at $n_H=n_E=10$: ten triangle hinges and ten edges.
Squared edge data live in $\mathrm{SqEdges}_4:=\mathrm{Fin},10\to\mathbb{R}$. To reuse a single seed-hinge dihedral formula, edges are pulled so that a chosen hinge $h$ occupies Gram seed slots $(0,1,2)$. The pull is encoded by a table $\mathrm{pullEdgeSlot}:\mathrm{Fin},10\to\mathrm{Fin},10\to\mathrm{Fin},10$; the remapped configuration is $e\mapsto a(\mathrm{pullEdgeSlot},h,e)$. By definition of that table, hinge $0$ pulls every slot to itself.
proof idea
Apply function extensionality on the edge index $e$. Unfold the remapping definition and the pull-slot table. The $h=0$ clause of the table is the identity map on slots, so both sides agree pointwise after simp.
why it matters
Feeds the immediate parent remapped_seed_dihedral_eq, which equates the seed dihedral angle of the zero-remapped configuration with that of the original edge data (one rewrite of this identity). That step is part of the THEOREM tier for seed-hinge dihedral derivatives and flat directional Schläfli kill along affine velocities through the flat seed (Gate A2-style input at flat, $n_H=n_E=10$).
It does not close the OPEN items in the module doc: full pathwise identity off the flat seed on nondegenerate 4-simplices, remapped HasDerivAt for every hinge row, elevation to a Regge candidate, or $S_{RS}\to$ Einstein–Hilbert in 4D. It is pure edge-slot bookkeeping, not a curvature or action statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.