seed_hinge_is_zero
plain-language theorem explainer
The seed hinge of the Freudenthal 4-simplex (hinge index 0) is the triangle on vertices 0, 1, 2. Anyone fixing the flat seed configuration or matching hinge rows to dihedral kernels cites this. The proof is pure definitional equality (rfl) against the triangle-index enumeration.
Claim. Under the local hinge enumeration of the Freudenthal 4-simplex, hinge index $0$ is the ordered vertex triple $(0,1,2)$.
background
The 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$). Hinges are the triangular 2-faces; edges run over a 10-slot squared-length coordinate chart.
localHinge is the local hinge map: it sends each of the ten hinge indices in $\mathrm{Fin},10$ to an ordered triple of vertices in $\mathrm{Fin},5 \times \mathrm{Fin},5 \times \mathrm{Fin},5$, implemented as triangleIndexTriple. The seed configuration is the flat 4-simplex at which areas, dihedral kernels, and the flat Schläfli summand table are evaluated.
Section §3 fixes the geometric match of the seed hinge row against hingeArea · angleKernel from the 4D dihedral kernel analysis.
proof idea
One-line definitional proof: rfl. Unfolding localHinge to triangleIndexTriple makes localHinge 0 = (0,1,2) hold by construction of the triangle-index table; no lemmas are applied.
why it matters
Pins the seed hinge as the reference triangle $(0,1,2)$ so later seed-hinge geometric match statements (flat area, dihedral HasDerivAt along squared-edge paths, and the flat directional Schläfli kill) have a fixed combinatorial anchor. The module tags this block as THEOREM material feeding the non-vacuous flat SchlaefliIdentityN witness at $n_H = n_E = 10$ and the Gate A2-style flat directional identity.
It does not close the OPEN items: full pathwise Schläfli off the flat seed on Nondeg4Simplex, remapped derivatives for every hinge row, elevation to the Regge candidate, or $S_{RS}\to$ Einstein–Hilbert in 4D. No downstream uses are recorded in the graph yet; the declaration is a local seed convention for the pathwise analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.