Pith. sign in
module module moderate

IndisputableMonolith.Geometry.DihedralCayleyMenger

show as:
view Lean formalization →

Bridges tetrahedral dihedral angles to the 5×5 Cayley–Menger matrix: vertex-to-matrix index maps, cofactor-ratio cosines, and arccos angles for a 3-simplex. Specializes cleanly on the regular unit tetrahedron under an explicit cofactor check. Cited by Regge deficit, dihedral-derivative, and cofactor-polynomial modules. Mostly definitions plus regular-case identities.

claimMap tetrahedron vertices $\{0,1,2,3\}$ to Cayley–Menger indices $\{1,2,3,4\}$ and form the squared cosine, cosine, and dihedral angle at an edge from $5\times 5$ CM cofactors and a positive denominator built from face minors. On the regular unit tetrahedron, under a named cofactor-check hypothesis, the cosine and angle reduce to explicit algebraic constants.

background

In 3D Regge calculus the deficit at a hinge is $2\pi$ minus the sum of dihedral angles of tetrahedra meeting there. Those angles are functions of the six squared edge lengths. The Cayley–Menger matrix packages those lengths into a $5\times 5$ bordered Gram-type matrix whose determinant is (a multiple of) the squared volume; its cofactors enter classical formulas for face areas and dihedral cosines.

Upstream, CayleyMengerMatrix ties the explicit cubic polynomial cm3 to that determinant/cofactor layer; DihedralAngle sets the general simplex dihedral interface (Phase C2 toward discharging Regge deficit linearization); ReggeRigorousFoundation supplies the polynomial and area identities needed for $M_{ij}=-\mathrm{area}(f_{ij})$.

This module is the concrete tetrahedron instance: index conventions (including opposite CM vertices), the denominator and cosine-squared expressions built from cofactors, the cosine and angle constructors, and a regular-unit cofactor check that pins the constant geometry of the equilateral case.

proof idea

Definition-first module, not a single deep theorem. It introduces index maps from tetrahedron vertices to CM rows/columns, opposite-vertex pairs for an edge hinge, then dihedralDenom3, dihedralCos3Sq, dihedralCos3, and dihedralAngle3 (arccos of the cofactor cosine) together with a bundled data record.

Regular-unit material is a small proof cluster: a cofactor-check proposition, a witness, and one-line (or short) specializations that, given the check, evaluate the cosine and angle on the regular unit tetrahedron to fixed values. No heavy tactic development lives here; algebraic content is deferred to cofactor-polynomial and Berger-formula modules.

why it matters in Recognition Science

This is the shared CM-to-dihedral API for the geometry stack. Downstream importers include DihedralCofactorFormula (Berger identification of geometric face-normal cosine with the CM cofactor ratio), DihedralDerivatives (chain rule $d\theta=-(1-\cos^2\theta)^{-1/2},d(\cos\theta)$), CofactorDerivatives and CofactorPolynomial (explicit partials of the same cofactors), and FourTetSignedDeficit (first kernel-checked signed Regge deficits on an abstract four-tet hinge star).

It also feeds the Lorentzian lane via CausalSimplexWick (CDT-style tetrahedron classes and kinematical Wick rotation in $D=3$). In the broader RS program this sits under the Regge component theorem foundation and the $D=3$ spatial forcing (T8), supplying the Euclidean hinge geometry that later deficit and gravity modules differentiate and assemble.

scope and limits

used by (6)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (13)