nondeg_flat
plain-language theorem explainer
The flat Freudenthal squared-edge assignment on the 4-simplex is nondegenerate: every edge length squared is positive and every triangle-hinge area is strictly positive. Anyone building a non-vacuous flat Schläfli witness at nH = nE = 10 cites this. The proof is a finite case split on edges plus a rewrite to the already-proved flat hinge-area positivity lemma.
Claim. Let $a$ be the flat Freudenthal squared-edge assignment on the 4-simplex (ten edges). Then $a$ is nondegenerate: $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
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 equal ten. Squared edge lengths live in SqEdges4 (maps Fin 10 → ℝ). The flat seed seedFlatSqEdges fixes the ten squared lengths to the standard Freudenthal pattern $(1,2,3,4,1,2,3,1,2,1)$; flatSqEdges is that same assignment.
Nondegeneracy of a squared-edge assignment $a$ is the structure Nondeg4Simplex a: every edge coordinate is positive, and every hinge area computed by Heron from the three boundary slots of that hinge is positive. Flat hinge areas are packaged as hingeAreaFlat, built from the three flat boundary squared lengths hingeFlatEdgeSq. The upstream lemma hingeAreaFlat_pos already shows each of those ten areas is a concrete positive constant ($1/2$, $\sqrt{2}/2$, $\sqrt{3}/2$, …).
The module’s binding tier requires a non-vacuous flat SchlaefliIdentityN witness with strictly positive areas, explicitly avoiding a zero-measure shell (lesson L-p1-schlaefli-not-vacuous-prop).
proof idea
Two structure fields, both by finite exhaustion.
For edge_pos: introduce an arbitrary edge index in Fin 10, case-split with fin_cases, unfold flatSqEdges to seedFlatSqEdges, and discharge each of the ten numerical inequalities $0 < 1,2,3,4,\ldots$ by norm_num.
For area_pos: introduce a hinge index $h$, rewrite the target area via hingeAreaFlat, hingeFlatEdgeSq, and flatSqEdges, then apply the already-proved hingeAreaFlat_pos h. No new area computation is done here; positivity is inherited.
why it matters
Without a strictly positive-area flat seed, any flat Schläfli identity at $n_H = n_E = 10$ would be vacuous (the zero-measure shell the module explicitly refuses). This theorem supplies the nondegeneracy certificate for flatSqEdges, which the module lists among its THEOREM-tier deliverables: “a non-vacuous flat SchlaefliIdentityN witness (strictly positive areas)”.
It sits under the broader Regge/Schläfli gravity analysis chain (hinge kernels, orbit classification, Hessian assembly) that feeds Gate-A2-style directional Schläfli kill at the flat seed and, eventually, the still-open pathwise identity off the flat seed on Nondeg4Simplex, elevation to a candidate, and $S_{RS}$ convergence to Einstein–Hilbert in 4D. It does not flip gap_action_recovery. In the Recognition forcing picture this is pure geometric scaffolding for the continuum limit, not a T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.