freudenthalTetSqEdges
plain-language theorem explainer
Squared edge lengths for every Freudenthal tetrahedron in the unit cube are the fixed 6-tuple (1, 2, 3, 1, 2, 1): three unit steps, two face diagonals, one body diagonal. Anyone citing Cayley–Menger volume or Regge edge bookkeeping on the six-tet cube uses this constant. It is a pure data definition by cases on the six edge slots.
Claim. The local squared-edge assignment for a unit-cube Freudenthal tetrahedron is the map $e\colon\{0,\ldots,5\}\to\mathbb{R}$ with $e(0)=1$, $e(1)=2$, $e(2)=3$, $e(3)=1$, $e(4)=2$, $e(5)=1$ (three unit edges, two face diagonals of squared length $2$, one body diagonal of squared length $3$).
background
The module fixes the standard Freudenthal decomposition of the unit cube into six tetrahedra along the body diagonal from vertex $0=(0,0,0)$ to $7=(1,1,1)$. Cube vertices are binary coordinates; the six tets are the monotone paths from $0$ to $7$.
Upstream, squared edge lengths of a tetrahedron are an assignment SqEdges $:= \mathrm{Fin},6\to\mathbb{R}$, the six independent edge slots that feed the Cayley–Menger polynomial. The present definition supplies the concrete lengths that every Freudenthal tet in the unit cube carries: three axis-aligned unit edges (squared length $1$), two face diagonals (squared length $2$), and the space diagonal (squared length $3$).
Those lengths are the local metric data against which global cube edges and later periodic/torus displacements are matched.
proof idea
Pure definitional assignment: six pattern-match arms on the edge index in $\mathrm{Fin},6$, returning the constants $1,2,3,1,2,1$ in order. No lemmas, no tactics.
why it matters
This constant is the metric seed for the whole Freudenthal incidence stack. It is the sqEdge field of the nondegenerate tet package, and the immediate theorem that the Cayley–Menger cubic evaluates to $8$ (hence positive volume) is a one-line unfold-and-norm on these six numbers.
Downstream, local-to-global edge equalities in the cube, the two-cube strip, and the periodic Freudenthal torus all reduce by case analysis to this table. In the gravity analysis layer the same lengths enter the raw cell stencil and Jacobian coefficients of the Regge TT Bloch interface audit, so continuum-limit and finite-difference identities inherit the unit-cube Freudenthal metric from here.
Within Recognition geometry this is scaffolding for discrete 3-space (primer T8, $D=3$) realized as a Regge complex rather than a continuum postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.