module module high

`IndisputableMonolith.Geometry.DihedralAngle`

This module supplies the basic data type for a dihedral angle in a simplicial complex, represented solely by its cosine restricted to the closed interval [-1, 1]. It is cited by the linearization and discharge phases that convert Regge deficits into curvature identities. The module itself contains only definitions and elementary bounds; it imports the Cayley-Menger volume formula and exports angle data to Schläfli, deficit linearization, and simplicial discharge modules.

claimA dihedral angle datum is a real number $c$ satisfying $-1 \le c \le 1$, interpreted as $\cos heta$ for the angle $ heta$ between two faces of a simplex.

background

The module sits inside the geometry layer that prepares simplicial complexes for Regge calculus. It depends on the Cayley-Menger module, whose determinant expresses the squared volume of an n-simplex from its edge lengths. DihedralAngleData is the sole exported type: a wrapper around a cosine value in [-1,1]. Sibling declarations supply the associated angle bounds (theta_nonneg, theta_le_pi) and concrete values for regular tetrahedra and cubes.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the geometric interface required by the three downstream phases that together discharge the ReggeDeficitLinearizationHypothesis. It is used directly by Schläfli (Phase C3), DeficitLinearization (Phase C4), and SimplicialDeficitDischarge (Phase C5), the last of which composes the earlier phases into a Lean statement of the paper's Theorem 5.1 (field-curvature identity).

scope and limits

Does not derive the cosine from edge lengths.
Does not relate the datum to volume or curvature.
Does not treat dihedral angles in dimensions other than three.
Does not encode orientation or signed angles.

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