hingeFlatEdgeSq
plain-language theorem explainer
For each of the ten triangle hinges of the Freudenthal 4-simplex, returns the three squared edge lengths of that hinge boundary at the flat seed. Area evaluations and the flat Schläfli summand table depend on it. The body looks up the three boundary slots and reads the flat seed edge vector.
Claim. For each hinge index $h \in \{0,\ldots,9\}$, return the triple $(e_{s_0}^2, e_{s_1}^2, e_{s_2}^2)$ of squared edge lengths on the flat seed configuration, where $(s_0,s_1,s_2)$ are the three boundary edge slots of hinge $h$ ordered as $(v_0v_1, v_0v_2, v_1v_2)$.
background
The module develops pathwise Schläfli identities for the Freudenthal (Kuhn) 4-simplex, the 4D analogue of the 3D Gate-A2 tetrahedron input. There are ten edges and ten triangle hinges ($n_H = n_E = 10$). Hinges are the 2-faces whose dihedral angles enter the Schläfli sum.
The flat seed is a fixed nondegenerate squared-edge assignment on those ten edges. Boundary edge slots of hinge $h$ are the three global edge indices that form the triangle of that hinge, ordered $(v_0v_1, v_0v_2, v_1v_2)$. The flat squared-edge vector is the constant seed assignment used for all flat evaluations.
This definition packages those two lookups into the three squared lengths needed by Heron's formula for the flat hinge area.
proof idea
Pure definitional packaging. Read the three boundary slots of hinge $h$, then evaluate the flat seed squared-edge vector at each slot, and return the resulting real triple. No arithmetic beyond indexing.
why it matters
Supplies the edge data for every flat hinge area. The immediate consumer is the flat hinge-area map, which feeds Heron evaluation and the explicit closed forms for hinges $0$ through $6$ (values such as $1/2$, $\sqrt{2}/2$, $\sqrt{3}/2$, $1$). Those areas are the positive weights in the flat Schläfli summand table and in the non-vacuous flat $\mathrm{SchlaefliIdentityN}$ witness at $n_H=n_E=10$.
Module tier tags mark flat hinge areas and the flat Schläfli summand table as THEOREM content; this definition is the edge-side input to that chain. It does not address the OPEN pathwise identity off the flat seed, remapped derivatives on every hinge row, or elevation to the Einstein-Hilbert candidate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.