Nondeg4Simplex
plain-language theorem explainer
Non-degeneracy for a Freudenthal 4-simplex given by ten squared edge lengths: every edge length squared is strictly positive, and every triangular hinge has strictly positive area via Heron. Anyone proving pathwise Schläfli off the flat seed cites this as the open domain. It is a pure Prop structure, no proof body.
Claim. A squared-edge assignment $a:\{0,\ldots,9\}\to\mathbb{R}$ is a nondegenerate 4-simplex if $a(e)>0$ for every edge $e$, and for every triangle-hinge $h$ the Heron area formed by the three boundary squared lengths of $h$ is strictly positive.
background
The module lifts the 3D Gate-A2 Schläfli input (six edges, six hinges) to the Freudenthal/Kuhn 4-simplex, where both the edge count and the triangle-hinge count equal ten. Squared edge data live in SqEdges4, i.e. maps $\mathrm{Fin},10\to\mathbb{R}$ in the local incidence slot order.
Each hinge $h$ has three boundary edge slots given by hingeBoundarySlots in order $(v_0v_1,v_0v_2,v_1v_2)$. The hinge area is $\sqrt{\mathrm{heronSq}(a,b,c)}$, the usual Heron square-root of the three squared side lengths. Nondegeneracy therefore means: no collapsed edge and no collapsed triangular face.
The module already proves a non-vacuous flat SchlaefliIdentityN witness and flat directional Schläfli kill. The open goal is the full pathwise identity on this nondegenerate locus, not merely on the flat seed.
proof idea
No proof: this is a structure extending Prop. The two fields are universal quantifiers over Fin 10 requiring strict positivity of squared edges and of Heron hinge areas assembled from hingeBoundarySlots and hingeArea. Downstream, nondeg_flat inhabits the structure on flatSqEdges by fin_cases plus norm_num on the seed table.
why it matters
This is the open domain named in the module's OPEN tier: full pathwise Schläfli identity off the flat seed is stated on Nondeg4Simplex, together with remapped HasDerivAt for every hinge row and the elevation path toward S_RS_converges_EH_4d. The immediate consumer is nondeg_flat, which shows the flat Freudenthal seed is a strictly positive-area witness, discharging the lesson that Schläfli identities must not live on a zero-measure shell.
In the gravity stack this keeps the 4D Regge/Schläfli analysis aligned with the 3D tetrahedron closed form: combinatorics and flat kernels are theorems; pathwise identity away from flat remains conditional on nondegeneracy. It does not touch gap_action_recovery or the Recognition forcing chain (T0–T8); it is pure discrete-geometry scaffolding for the Einstein–Hilbert continuum limit of the RS action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.