Pith. sign in
module module moderate

IndisputableMonolith.Geometry.AffineIndepInterior

show as:
view Lean formalization →

Infrastructure for tetrahedral face normals in Euclidean 3-space: coordinate vectors are cast to Mathlib's ℓ² inner-product type, adjacent face normals are built from edge-vector cross products, and linear independence of those edges forces the normals to be nonzero and non-parallel. Anyone proving dihedral cosines stay in (−1,1) or feeding Regge/Schläfli smoothness cites this. The module is mostly definitional plus elementary inner-product and cross-product lemmas.

claimMap coordinate triples into Euclidean $\mathbb{R}^3$ with the standard inner product; form adjacent face normals $n_i,n_j$ by cross products of edge vectors; prove that linear independence of the edge frame implies $n_i\neq 0$, $n_i\times n_j\neq 0$, and $\frac{n_i\cdot n_j}{\|n_i\|\|n_j\|}\notin\{\pm 1\}$.

background

Recognition Science geometry for discrete gravity works with tetrahedra whose edge lengths determine dihedral angles via the normalized inner product of outward face normals. The upstream DihedralCofactorFormula module sets that geometric cosine (normals from cross products, then the normalized pairing) as the Euclidean side of the Berger cofactor identity that will match Cayley–Menger cofactors.

This module supplies the Euclidean embedding layer: a cast toEuclidean3 that views a coordinate vector as Mathlib's ℓ² vector so inner products, norms, and scalar multiplications are the standard ones. Adjacent face normals are assembled from edge vectors; independence of those edges is the nondegeneracy hypothesis that keeps the tetrahedron from collapsing and keeps face normals well-defined and non-parallel.

The local setting is therefore the open cone of nondegenerate tetrahedral edge data, where dihedral cosines are strictly inside $(-1,1)$ and arccos is smooth.

proof idea

Definitional core: embed coordinates into Euclidean 3-space and record the usual identities (inner product of the cast equals the coordinate dot product; squared norm; homogeneity under scalar multiplication). Independence lemmas then show that if two edge vectors are linearly independent, the corresponding face normal (their cross product) is nonzero, and that adjacent face normals are linearly independent if and only if their cross product is nonzero. Separate lemmas convert linear independence into the strict inequalities that the normalized dot product is neither $+1$ nor $-1$, which is exactly the condition that arccos stays away from the branch points. No deep theorem is proved here; the module packages standard $\mathbb{R}^3$ linear algebra for downstream geometric analysis.

why it matters in Recognition Science

ReggeActionSmoothness imports this module because the full nonlinear Regge action needs the conformal edge chart to remain in the nondegenerate tetrahedral cone and the arccos arguments to stay away from $\pm 1$ so the finite action is smooth at the flat potential. SchlaefliTetrahedronProof likewise needs well-defined, nondegenerate dihedral data when it connects Cayley–Menger and dihedral derivatives to the local tetrahedral Schläfli package.

In the broader RS geometry stack this is the Euclidean nondegeneracy gate in front of the Berger cofactor formula and the closed-form Schläfli identity: without independent adjacent face normals the dihedral cosine is undefined or extremal, and smoothness or closed-form derivative identities fail. It does not itself state the cofactor or Schläfli theorems; it only guarantees the geometric hypotheses those theorems consume.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (28)