freudenthalRealizedTet
plain-language theorem explainer
Packages the four explicit one-cube Freudenthal vertices in R^3 as a realized tetrahedron, with affine independence already discharged. Gravity and Regge-calculus workers cite it whenever a concrete nondegenerate chart is needed on the periodic cubic lattice. The body is a one-line application of the affine-independence theorem to the generic constructor.
Claim. Let $p_0,\ldots,p_3\in\mathbb{R}^3$ be the standard one-cube Freudenthal vertex coordinates. The four-point map $p:\mathrm{Fin}\,4\to\mathbb{R}^3$ is affinely independent, and the pair $(p,\text{affine independence})$ is the realized tetrahedron used as the local geometric chart.
background
The module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not claim the Dirichlet equality outright; it packages the exact obligations needed to instantiate that model on a periodic Freudenthal torus.
A realized tetrahedron is four points in Euclidean 3-space together with an affine-independence certificate. That certificate later feeds strict dihedral-range and positive-volume arguments. The Freudenthal one-cube triangulation supplies a fixed coordinate chart on each of the six tets that fill the unit cube; the squared-edge lengths of that chart are the classical Freudenthal edge tuple.
Upstream, affine independence of the explicit coordinates is already proved: after reindexing the three nonzero vertices, the coordinate matrix is upper triangular with diagonal ones. A companion constructor turns any such independence proof into a realized tetrahedron.
proof idea
One-line wrapper. Apply the constructor that builds a realized tetrahedron from an affine-independence hypothesis, feeding it the already-proved independence of the explicit Freudenthal realization points. No further algebra is performed at this site.
why it matters
This definition is the concrete local chart that discharges the geometric side of the canonical periodic flat-configuration inputs: those inputs combine the explicit Freudenthal tetrahedron with a certified global zero-deficit angle-sum chain. Downstream, the squared-edge map of this realization is identified with the classical Freudenthal edge tuple (no residual independence hypothesis), and every encoded tetrahedron at canonical periodic flatness is shown to carry that same edge tuple.
In the broader gravity stack this pins the local geometry of the six-tet cubic Dirichlet instance used for Regge action and finite-difference Dirichlet targets on the periodic lattice. It sits under the physical six-tet model rather than under the T0–T8 forcing chain, but it is the geometric substrate those Dirichlet and Regge limits act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.