freudenthalRealizationPoints
plain-language theorem explainer
Explicit Euclidean coordinates for the standard one-cube Freudenthal tetrahedron: (0,0,0), (1,0,0), (1,1,0), (1,1,1) in R^3. Anyone assembling a realized tet, checking affine independence, or feeding the Regge-to-Dirichlet continuum limit on the periodic Freudenthal torus cites this map. It is a pure pattern-match definition on Fin 4, with squared edge lengths (1,2,3,1,2,1) in tetrahedral edge order.
Claim. Define four points in Euclidean $\mathbb{R}^3$ by $p_0=(0,0,0)$, $p_1=(1,0,0)$, $p_2=(1,1,0)$, $p_3=(1,1,1)$. In the standard tetrahedral edge order the squared edge lengths are $(1,2,3,1,2,1)$.
background
The module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it supplies the geometric and analytic ingredients that make that equality a theorem once the named hypotheses hold.
A Freudenthal triangulation of the unit cube decomposes it into six tetrahedra. The one-cube Freudenthal tetrahedron is the simplex with vertices at the origin and the three successive partial sums of the standard basis of $\mathbb{R}^3$. The squared edge lengths in tetrahedral edge order are then $(1,2,3,1,2,1)$, matching the combinatorial Freudenthal edge tuple used elsewhere in the gravity stack.
Downstream constructions treat these four points as a RealizedTet once affine independence is supplied, and feed that realization into the nonlinear Regge finite-aggregate limit toward Dirichlet energy.
proof idea
No proof: the declaration is a definition by cases on Fin 4. Vertex 0 is the origin; vertex 1 is the first standard basis vector; vertex 2 is the sum of the first two; vertex 3 is the sum of all three. Each value is built from EuclideanSpace.single additions in $\mathbb{R}^3$.
why it matters
This coordinate chart is the concrete geometric seed for the physical six-tet cubic Dirichlet instance. It is the point map assumed affinely independent in the full nonlinear Regge finite-aggregate theorem that sends the variable-weighted probe spacing to Dirichlet energy under zero deficit. It is also the input to the affine-independence theorem (upper-triangular coordinate matrix after reindexing nonzero vertices), and to the two constructors that package the points as a realized tet and verify that the squared-edge tuple matches the combinatorial Freudenthal edges.
In the broader Recognition gravity program this closes the local geometry side of the encoded periodic Freudenthal torus scaffold: once the four points are fixed and shown nondegenerate, the remaining work is analytic (stencil correspondence, continuum limit, zero-deficit input), not a further choice of embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.