oppFlatSqEdges
plain-language theorem explainer
Flat squared-edge assignment for an opposite-orbit Freudenthal 4-simplex on the seed hinge: the ten values (1,2,2,1,1,3,2,4,3,1). Every opposite-class Gram, apex-norm, and dihedral identity in the star kernel cites it as the Euclidean base point. Pure data definition by case split on the ten edge slots.
Claim. Define the flat squared-edge map $e_{\mathrm{opp}}:\{0,\ldots,9\}\to\mathbb{R}$ by $e_{\mathrm{opp}}(0)=1$, $e_{\mathrm{opp}}(1)=2$, $e_{\mathrm{opp}}(2)=2$, $e_{\mathrm{opp}}(3)=1$, $e_{\mathrm{opp}}(4)=1$, $e_{\mathrm{opp}}(5)=3$, $e_{\mathrm{opp}}(6)=2$, $e_{\mathrm{opp}}(7)=4$, $e_{\mathrm{opp}}(8)=3$, $e_{\mathrm{opp}}(9)=1$. This is the Euclidean edge-length-squared vector of an opposite-orbit 4-simplex in the seed-hinge star, in the local edge-slot order of the incidence layer.
background
The module builds the full periodic-lattice star deficit kernel for the seed triangle hinge ${0,e_0,e_0+e_1}$ in the 4D Freudenthal triangulation: four containing unit cubes and six incident 4-simplices. It sits one layer above the two-simplex dihedral cosine calculus and the 15-class edge stencil.
Squared edge data for a 4-simplex are packaged as a map from ten slots to $\mathbb{R}$ (the type SqEdges4). The upstream dihedral kernel records that the flat Freudenthal squared lengths shared by both seed simplices live in the local slot order of the incidence layer. The star splits those six simplices into opposite and orthogonal orbits; this definition is the opposite-orbit Euclidean base point.
Sibling data give the orthogonal flat assignment. Downstream numerics evaluate Gram determinants, apex norms, and dihedral cosines on this vector.
proof idea
No proof: a total function on Fin 10 defined by ten literal real constants via pattern match. The values are the squared edge lengths of a unit-cube Freudenthal 4-simplex in the opposite orbit, written in the fixed local edge-pair ordering.
why it matters
This is the Euclidean base configuration for the opposite orbit in deliverable A of the star kernel. It feeds hingeGramDet_opp (value 4), the three apex numerator identities, and cosDihedral_opp_flat, which proves the flat dihedral cosine equals $1/\sqrt{2}$. That cosine is half of the flat multiset (four simplices at $1/\sqrt{2}$, two at 0) used to gate star angle sum $2\pi$ and the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$.
Coordinate paths and slotwise derivative theorems (oppCoordPath, hasDerivAt_opp_coord) also start from these ten numbers, so the opposite-class contribution to the flat Hessian stencil is anchored here. The module still does not assemble the Hessian over all hinge orbits, nor prove $S_{RS}$ converges to Einstein–Hilbert in 4D, nor flip gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.