Pith. sign in
module module moderate

IndisputableMonolith.Geometry.AffineIndepInterior

show as:
view Lean formalization →

Infrastructure for nondegenerate tetrahedral geometry in Euclidean 3-space: coordinate vectors as Mathlib ℓ² vectors, adjacent face normals from edge crosses, and linear-independence criteria that keep normalized normal dots strictly inside (−1,1). Cited by Regge smoothness and the closed-form Schläfli package. Mostly embedding lemmas plus cross-product independence equivalences.

claimMap coordinate triples into Euclidean $\mathbb{R}^3$ so that the Mathlib inner product recovers the geometric dot product; for a tetrahedron, form adjacent face normals $n_i,n_j$ via edge-vector crosses and prove that linear independence of the edge frame is equivalent to $n_i\times n_j\neq 0$, hence $\langle\hat n_i,\hat n_j\rangle\notin\{\pm 1\}$.

background

Recognition Science geometry work on tetrahedra needs a clean bridge between abstract coordinate data and Mathlib's Euclidean inner-product API. This module supplies that bridge: a view toEuclidean3 that treats a coordinate vector as an $\ell^2$ vector, with companion facts for inner products, squared norms, and scalar multiplications.

Upstream, DihedralCofactorFormula defines the geometric side of the tetrahedral dihedral cosine: face normals from cross products and the normalized inner product of two adjacent face normals, aimed at the Berger cofactor identification with a Cayley–Menger cofactor. Nondegeneracy of that cosine (arguments of $\arccos$ away from $\pm 1$) is exactly the independence of those normals.

Locally the module packages adjacent-face-normal constructions and predicates such as AdjacentFaceNormalsIndependent, together with equivalences linking edge-vector linear independence, nonzero face normals, and nonzero crosses of adjacent normals.

proof idea

Definition-and-lemma layer rather than a single deep theorem. Embedding facts for toEuclidean3 are direct rewrites against Mathlib's Euclidean structure (inner product, norm squares, homogeneity under scalar multiplication). Independence statements reduce normalized dots $\langle u,v\rangle/(\lVert u\rVert\lVert v\rVert)$ away from $\pm 1$ once $u,v$ are linearly independent and nonzero. Face-normal nonvanishing follows from linear independence of the spanning edge vectors; the key equivalence identifies AdjacentFaceNormalsIndependent with the cross product of the two normals being nonzero, which is the standard 3D criterion for non-parallel planes.

why it matters in Recognition Science

Feeds two geometry parents. ReggeActionSmoothness needs the conformal edge chart to stay in the nondegenerate tetrahedral cone and arccos arguments away from $\pm 1$ so the finite nonlinear Regge action is smooth at the flat potential; the independence lemmas here are exactly those cone and cosine guards. SchlaefliTetrahedronProof connects Cayley–Menger and dihedral derivatives to the local tetrahedral Schläfli package; it imports this module so geometric normals and their independence sit under the closed-form identity rather than an external field. In the broader RS chain this is classical Euclidean scaffolding for discrete curvature (Regge/Schläfli), not a forcing-step (T0–T8) claim.

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)