module module high

`IndisputableMonolith.Geometry.DihedralAngle`

The DihedralAngle module encodes dihedral angle data as a cosine value in the closed interval [-1, 1] and supplies elementary bounds plus explicit values for regular tetrahedra and cubes. It is cited by researchers formalizing Regge calculus on piecewise-flat simplicial complexes. The module consists of definitions and direct verifications with no non-trivial proofs.

claimA dihedral angle is represented by its cosine $c$ satisfying $-1 < c < 1$. The module also records the explicit cosine for the regular tetrahedron dihedral angle and for the cube dihedral angle.

background

This module sits inside the simplicial geometry layer that supports the Recognition Science program for discharging the Regge deficit linearization hypothesis. It builds directly on the Cayley-Menger module, which encodes the volume of an n-simplex from its edge lengths via the Cayley-Menger determinant. Dihedral angles arise at the codimension-1 faces where two simplices meet; their cosines enter the deficit angle that measures local curvature. The module introduces the data type whose only field is the cosine together with the elementary facts that this cosine is non-negative, at most 1, and equals the known algebraic values for the regular tetrahedron and the cube.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The primitives supplied here are imported by the Schläfli identity module (Phase C3), the Piran-Williams deficit linearization module (Phase C4), and the simplicial deficit discharge module (Phase C5). These three phases together compose the general discharge of the ReggeDeficitLinearizationHypothesis that yields the field-curvature identity of Theorem 5.1. The module therefore closes the geometric interface between edge-length data and curvature deficits in the D=3 simplicial setting.

scope and limits

Does not compute dihedral angles from edge lengths.
Does not treat non-simplicial polyhedra.
Does not extend to dihedral angles in dimension greater than 3.
Does not contain Schläfli's identity or deficit linearization.

used by (3)

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

IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge module_import
IndisputableMonolith.Geometry.DeficitLinearization module_import
IndisputableMonolith.Geometry.Schlaefli module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMenger module_import

declarations in this module (17)

structure DihedralAngleData L56
theorem theta_nonneg L65
theorem theta_le_pi L68
theorem cos_theta L72
def regular_tet_dihedral L79
theorem regular_tet_dihedral_theta L86
theorem regular_tet_dihedral_in_open_interval L90
def cube_dihedral L105
theorem cube_dihedral_theta L112
def sumThetas L126
def FlatSumCondition L130
def deficit L134
theorem deficit_eq_zero_of_flat L138
theorem cubic_lattice_flatSum L145
theorem cubic_lattice_deficit_zero L154
structure DihedralAngleCert L160
theorem dihedralAngleCert L171