flatSqEdges_eq_seed
plain-language theorem explainer
The local flat squared-edge 10-vector on the Freudenthal 4-simplex is definitionally identical to the seed flat squared lengths from the dihedral-kernel layer. Anyone assembling flat hinge areas or the flat Schläfli summand table cites this to lock the edge coordinates. The proof is pure reflexivity: the local name is an alias of the seed.
Claim. The flat squared-edge assignment on the 4-simplex equals the seed flat squared lengths in local edge-slot order: $(1,2,3,4,1,2,3,1,2,1)$.
background
This module lifts the 3D Gate-A2 Schläfli input (six edges, six hinges on a tetrahedron) to the Freudenthal/Kuhn 4-simplex, where both the edge count and the triangle-hinge count are ten. Work is staged at the flat seed first: squared edge lengths, hinge areas, and directional derivatives along affine paths through that seed.
The seed flat squared lengths are the ten numbers shared by both seed simplices, ordered by the incidence layer's local edge pairing: slots map to $1,2,3,4,1,2,3,1,2,1$. The local name flatSqEdges is introduced in this file simply as that same 10-tuple, so downstream flat geometry (hinge boundary slots, flat areas via Heron, column sums of the Schläfli table) can refer to a module-local symbol without importing the kernel name at every use site.
Upstream, the dihedral-kernel module records those lengths as the common flat metric; the gluing/hinge witnesses supply the combinatorial edge and hinge faces that justify the ten-slot indexing.
proof idea
One-line term proof by rfl. The local flat squared-edge definition is literally := seedFlatSqEdges, so equality is definitional and needs no rewriting or case split on the ten Fin indices.
why it matters
Pins the flat metric coordinate that every flat Schläfli summand in this file reads. The module's binding tier tags require: flat hinge areas, a non-vacuous flat SchlaefliIdentityN witness at $n_H=n_E=10$ with strictly positive areas, seed-hinge HasDerivAt along every squared-edge path, and flat directional Schläfli kill along every affine velocity through the seed (Gate A2-style at flat). All of those rows evaluate edge lengths through this vector.
No downstream theorems currently list this equality as a named dependency (callers can unfold either name), but the alias keeps the pathwise file self-contained. It does not touch the open off-seed pathwise identity on nondegenerate 4-simplices, remapped derivatives for every hinge row, elevation to the Regge candidate, or $S_{RS}\to$ Einstein-Hilbert convergence in 4D. It also does not flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.