RealizedTet
plain-language theorem explainer
Packages a Euclidean tetrahedron as four points in R^3 together with affine independence. Geometry and Regge-calculus developments cite it whenever edge vectors, face normals, Gram determinants, or dihedral data must sit on a non-flat simplex. There is no proof body: the structure is the data carrier that later positive-volume and strict-dihedral arguments consume.
Claim. A realized tetrahedron is a map $p : \{0,1,2,3\} \to \mathbb{R}^3$ whose four image points are affinely independent over $\mathbb{R}$.
background
The module bridges the abstract six squared-edge coordinates of the Cayley–Menger layer to concrete point configurations in Euclidean 3-space. Mathlib supplies EuclideanSpace ℝ (Fin 3) and AffineIndependent, so the ambient geometry is ordinary inner-product 3-space rather than an abstract metric complex.
Affine independence of four points is exactly the condition that they do not lie in a common plane: the three edge vectors from any vertex form a basis of $\mathbb{R}^3$. The doc-comment keeps this hypothesis explicit so that later strict dihedral-range and positive-volume proofs can invoke it without re-deriving nondegeneracy.
Sibling definitions in the same file (edgeVector, gram3, volumeSqFromGram, volumeSqFromCM) read lengths and volumes off a RealizedTet, connecting the point model back to the Cayley–Menger polynomial used upstream in the Regge foundation.
proof idea
No proof: this is a structure declaration. The first field stores the four vertices as a function Fin 4 → EuclideanSpace ℝ (Fin 3). The second field is a proposition asserting affine independence of that point map. Downstream lemmas unpack these fields and never reconstruct the carrier.
why it matters
Every local Euclidean tetrahedron argument in the geometry stack takes a RealizedTet as input. Downstream, AffineIndepInterior builds adjacent face normals, proves their cross product equals a scalar triple product times the shared edge, and shows affine independence implies face-normal linear independence for every edge. That independence is the exact local condition excluding arccos endpoint cases, so dihedral cosines land in the open interval needed for interior Regge hinges.
In the broader Recognition framework this sits under the D = 3 landmark (forcing chain T8): tetrahedra are the 3-simplices of the discrete geometry that carries ledger and posting data. The structure does not itself force dimension three; it assumes the ambient Euclidean 3-space already fixed by the module imports and the Cayley–Menger setup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.