flatSqEdges
plain-language theorem explainer
Names the flat Freudenthal squared-edge configuration on the 4-simplex as the ten-slot map already fixed by the dihedral-kernel seed. Gravity analysts cite it whenever hinge areas, Schläfli summands, or directional derivatives are evaluated at the flat point. The body is a one-line alias of that seed vector.
Claim. Let $\mathrm{SqEdges}_4 := \mathrm{Fin}\,10\to\mathbb{R}$ be the space of squared edge lengths on a 4-simplex. Define the flat configuration $\ell^\flat\in\mathrm{SqEdges}_4$ to be the seed flat Freudenthal lengths $(1,2,3,4,1,2,3,1,2,1)$ in local edge-slot order.
background
This module lifts the 3D Gate-A2 Schläfli closed form from the tetrahedron ($n_H=n_E=6$) to the Freudenthal/Kuhn 4-simplex ($n_H=n_E=10$). Squared edge lengths are the natural Regge coordinates: $\mathrm{SqEdges}_4$ is simply $\mathrm{Fin},10\to\mathbb{R}$.
Upstream, the dihedral-kernel layer already fixes a concrete flat seed: ten positive squared lengths shared by both seed simplices, ordered by the incidence map localEdgePair. That seed is the unique flat reference against which hinge areas, angle kernels, and directional Schläfli identities are evaluated.
The present definition merely re-exports that seed into the pathwise Schläfli module so local lemmas can name a single flat point without importing the kernel namespace at every use site.
proof idea
One-line definitional alias: the pathwise flat edge map is definitionally equal to the upstream seed flat squared-edge vector. No computation or proof obligation; equality to the seed is immediate by rfl in the companion lemma.
why it matters
Every flat hinge-area evaluation in this file (hingeAreaFlat_0 through the remaining hinge indices) unfolds through this name, then through the seed, into Heron formulas that produce the strictly positive areas needed for a non-vacuous flat SchlaefliIdentityN witness at $n_H=n_E=10$.
That witness is a binding THEOREM tier of the module: column sums vanish and the seed-hinge row matches area times angle kernel. The same flat point is the base of every affine velocity for the directional Schläfli kill (Gate A2-style input at flat) and for HasDerivAt of seed-hinge dihedral angles along squared-edge paths.
It does not close the OPEN items (full pathwise identity off the flat seed, elevation to the EH candidate, or $S_{RS}$ convergence). It also does not touch gap_action_recovery. Within Recognition gravity it is the concrete flat 4D Regge background on which the Schläfli calculus is pinned before curvature is turned on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.