Pith. sign in
module module moderate

IndisputableMonolith.Geometry.ReggeRigorousFoundation

show as:
view Lean formalization →

Foundation layer for rigorous single-tetrahedron Regge calculus in three dimensions. It fixes non-degenerate edge data, model unit tetrahedra, conformal edge deformations, and the local Schläfli scaffolding that later modules lift to triangulations and dihedral formulas. Anyone matching Cayley-Menger gradients to face areas or dihedral derivatives cites this base. Content is mostly definitions plus smoothness certificates on the explicit CM polynomial and its partials.

claimA non-degenerate tetrahedron is six positive squared edge lengths whose Cayley-Menger determinant yields positive volume. The module supplies model configurations (regular and right-angled unit tets), conformal squared-edge paths $a_i(t)$, $C^\infty$ regularity of $\mathrm{CM}_3$ along those paths, and the local 3D Schläfli structure linking $dV$ to edge lengths and dihedral angles.

background

Regge calculus discretizes gravity on a triangulation whose metric data are edge lengths. For a single tetrahedron the six squared lengths determine the volume through the Cayley-Menger polynomial $\mathrm{CM}_3$; the classical relation is $V^2 = \mathrm{CM}_3/288$. Dihedral angles and their derivatives with respect to edges are the ingredients of the Regge action and of its second variation.

Upstream, the explicit polynomial $\mathrm{CM}_3$ and its six partials $\partial\mathrm{CM}_3/\partial a_i$ are already available as polynomial functions of the squared edges, together with a Taylor identity for $\mathrm{cm3}(a+h)$. The present module sits on that algebraic layer and packages the geometric hypotheses needed before one can talk about dihedral cosines, Euclidean realizations, or finite 3D triangulations.

The local theoretical setting is Euclidean 3-space tetrahedra with positive edge lengths, prepared so that later work can compare the genuine Regge Hessian entries $M_{ij}$ componentwise against face areas.

proof idea

Definition-and-certificate module rather than a single deep theorem. It introduces the non-degeneracy predicate on six edge lengths, two concrete model tetrahedra (regular unit and right-angled unit), incidence helpers for edges and opposite vertices, and conformal squared-edge deformations $a_i(t)$. Smoothness of those paths and of $\mathrm{CM}_3$ along them is recorded via Mathlib ContDiff facts built from the imported CM polynomial and derivative API. A named certificate aggregates the local foundation obligations for downstream import.

why it matters in Recognition Science

This is the shared base for the rigorous Regge program that aims to match the second-variation matrix from Cayley-Menger and dihedral derivatives against face areas. Downstream, dihedral cosines are defined from Cayley-Menger cofactors; the single-tetrahedron Schläfli identity is pinned in Regge notation (including $V^2=\mathrm{cm3}/288$); abstract edge coordinates are realized by points in $\mathbb{R}^3$; and finite 3D Regge triangulations lift the local identities. The gravity lane also imports it for causal (CDT-style) tetrahedron classes and the kinematical Wick rotation in $D=3$. Without this foundation layer those modules would re-state non-degeneracy, model tets, and conformal regularity ad hoc.

scope and limits

used by (5)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)