Pith. sign in
module module moderate

IndisputableMonolith.Geometry.ReggeRigorousFoundation

show as:
view Lean formalization →

Foundation layer for rigorous 3D Regge calculus on a single tetrahedron: non-degeneracy, model unit tets, dihedral structure, conformal edge deformations, and the local Schläfli identity. Downstream geometry and gravity modules import it to lift Cayley–Menger data to dihedral cosines, triangulations, Euclidean realizations, and Lorentzian CDT classes. The module packages definitions, smoothness facts, and a certificate rather than a single deep theorem.

claimRigorous single-tetrahedron setup for 3D Regge calculus: non-degenerate tets with positive edge lengths; regular and right-angle unit models; dihedral data on the six edges; conformal squared-edge paths $a(\varepsilon)$ with $C^\infty$ Cayley–Menger response; and the local 3D Schläfli identity linking volume variation to edge lengths and dihedral angles.

background

Recognition Science’s discrete-gravity lane needs a fully certified Regge layer, not prose. Upstream, CayleyMengerPolynomial supplies the explicit degree-3 Cayley–Menger polynomial $\mathrm{CM}3$ in the six squared edge lengths of a tetrahedron, aimed at comparing the genuine Regge second-variation matrix $M{ij}$ to face areas. CayleyMengerDerivatives then gives the six partials $\partial\mathrm{CM}_3/\partial a_i$ and the polynomial Taylor identity for $\mathrm{cm3}(a+h)$.

This module sits on that algebraic base and fixes the geometric objects those identities act on: a non-degenerate tetrahedron (positive edges, positive volume), standard model tets (regular unit and right-angle unit), edge-vertex incidence, and a dihedral structure. It also introduces conformal squared-edge deformations $a\mapsto a(\varepsilon)$ so that smoothness of $\mathrm{cm3}$ along those paths is available for calculus identities (volume-squared $V^2=\mathrm{cm3}/288$, Schläfli).

The setting is Euclidean 3-simplices before triangulation glueing or Lorentzian signature change; $D=3$ matches the forced spatial dimension in the RS forcing chain.

proof idea

Definition-and-certificate module, not one monolithic proof. It declares non-degeneracy and model tetrahedra, packages dihedral and edge-incidence structure, and proves continuity/$C^\infty$ facts for conformal squared-edge maps and for $\mathrm{cm3}$ along them (via Mathlib contDiff/exp/pow calculus and the upstream Cayley–Menger derivative API). The local Schläfli 3D identity is stated in the notation needed by later Regge component theorems. A top-level certificate aggregates the foundation claims for downstream import.

why it matters in Recognition Science

Closes the gap between raw Cayley–Menger algebra and usable Regge geometry. DihedralCayleyMenger imports it to define tetrahedral dihedral cosines from CM cofactors; SchlaefliTetrahedron pins the local Schläfli identity and $V^2=\mathrm{cm3}/288$; TetrahedronRealization connects six squared-edge coordinates to points in $\mathbb{R}^3$; ReggeTriangulation3D lifts local tet identities to finite 3D triangulations.

On the gravity side, CausalSimplexWick (QG Seven-Gaps, Lorentzian lane) builds CDT-style causal tet classes and kinematical Wick rotation on this Euclidean foundation. Without a certified non-degenerate tet, dihedral structure, and smooth conformal edge calculus, the componentwise $M_{ij}$ vs area comparison that motivated the Cayley–Menger program cannot be stated rigorously. Landmark tie-in: supports the discrete $D=3$ geometry forced at T8 once the continuum limit is taken.

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)