SqEdges4
plain-language theorem explainer
Squared edge-length data for a Freudenthal 4-simplex: a real value on each of the ten edge slots. Re-exported from the 4D dihedral kernel so the pathwise Schläfli module can name configurations, affine paths through the flat seed, and nondegeneracy without repeating the Fin-10 type. Pure abbreviation; no proof content.
Claim. Write $\mathrm{SqEdges}_4$ for the space of real assignments to the ten edge slots of a 4-simplex, i.e. maps $\{0,\ldots,9\}\to\mathbb{R}$ interpreted as squared edge lengths in the local incidence order.
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. Combinatorially one has $n_H=n_E=10$: ten triangle hinges and ten edges.
Upstream, the dihedral-kernel layer fixes the type of squared-edge configurations as maps from ten slots to $\mathbb{R}$, with a distinguished flat seed of Freudenthal squared lengths in the local edge-pair order. This module simply reuses that type under a short local name.
Squared lengths (not lengths) are the natural coordinates: hinge areas via Heron, Gram data for dihedral cosines, and affine paths through the flat seed are all written in those coordinates.
proof idea
One-line abbreviation re-exporting ReggeHinge4DDihedralKernel.SqEdges4, itself defined as Fin 10 → ℝ. No tactics, no lemmas.
why it matters
Local type spine for the entire pathwise 4D Schläfli development. Downstream definitions and theorems take configurations of this type: the flat seed, affine paths through flat in a squared-edge velocity, hinge-remapped configurations, the nondegenerate 4-simplex predicate (strictly positive edges and hinge areas), and the pathwise flat remainder comparing a candidate Jacobian to the flat Schläfli table.
That infrastructure supports the module's proved tier (flat Schläfli summand table, non-vacuous flat identity witness, seed-hinge HasDerivAt, flat directional Schläfli kill) and the still-open full pathwise identity off the flat seed, remapped derivatives on every hinge row, and elevation toward the 4D Einstein–Hilbert continuum limit. It does not touch gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.