hingeBoundarySlots_zero
plain-language theorem explainer
For the seed hinge (index 0) of the Freudenthal 4-simplex, the three boundary edge slots are the global edge indices 0, 1, and 4. Combinatorialists and Regge-calculus workers cite this when wiring hinge areas and dihedral kernels to the ten-edge coordinate chart. The proof is a three-way reflexivity check against the lookup table.
Claim. Writing $B(h,i)$ for the $i$-th boundary edge slot of hinge $h$ (ordered $(v_0v_1,v_0v_2,v_1v_2)$), one has $B(0,0)=0$, $B(0,1)=1$, and $B(0,2)=4$ in the standard $n_E=10$ edge indexing of the 4-simplex.
background
The module develops the pathwise Schläfli identity for the Freudenthal/Kuhn 4-simplex at $n_H=n_E=10$, mirroring the 3D Gate-A2 tetrahedron input. Hinges are the ten triangular faces; each hinge has three boundary edges that determine its area and feed the dihedral angle kernel.
The definition hingeBoundarySlots is the fixed lookup table sending a hinge index $h\in\mathrm{Fin},10$ and a local edge index $i\in\mathrm{Fin},3$ to a global edge index in $\mathrm{Fin},10$, ordered as $(v_0v_1,v_0v_2,v_1v_2)$. Seed hinge $h=0$ is the reference row used by flat-area and angle-kernel assembly.
Local theoretical setting (module doc): THEOREM-tier combinatorics for edges and triangle-hinges, flat hinge areas, and the flat Schläfli summand table; OPEN off the flat seed on Nondeg4Simplex.
proof idea
One-line term proof: the conjunction of three definitional equalities, each discharged by rfl against the pattern-match clauses of hingeBoundarySlots for hinge index 0.
why it matters
Pins the seed-hinge boundary wiring that every flat-area and dihedral-kernel computation in this module reads. Downstream assembly of flat hinge areas, the Schläfli summand table, and the Gate-A2-style directional kill along affine velocities through the flat seed all depend on knowing that hinge 0 sits on global edges 0, 1, 4.
No used_by edges are recorded yet; the declaration is infrastructure for the THEOREM-tier items listed in the module doc (flat Schläfli summand table, seed-hinge row matching hingeArea · angleKernel, non-vacuous SchlaefliIdentityN witness). It does not touch the OPEN pathwise identity off the flat seed, nor gap_action_recovery or $S_{RS}\to EH$ convergence. In the broader RS gravity stack this is pure Regge combinatorics supporting the 4D Schläfli input, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.