module module high

`IndisputableMonolith.Gravity.ReggeCalculus`

The ReggeCalculus module supplies the geometric primitives for discrete gravity within Recognition Science: 4-simplices fixed by 10 edge lengths, triangles, tetrahedra, dihedral angles, and deficit angles. Discrete gravity researchers and convergence proofs cite these structures as the starting point for Regge actions. The module consists of definitions plus elementary lemmas on flat configurations and deficit signs.

claimA 4-simplex has five vertices and ten edges whose lengths determine the geometry completely. Dihedral angles at hinges are obtained from the edge lengths via the cosine law; the deficit angle at each hinge is $2π$ minus the sum of the dihedral angles around that hinge.

background

This module works inside the Recognition Science treatment of gravity by replacing continuum manifolds with simplicial complexes. It defines Simplex4D as the basic 4-dimensional building block whose shape is fixed by its ten edge lengths, together with the lower-dimensional faces Triangle and Tetrahedron. HingeData packages an edge together with its incident dihedral angles, while deficit_angle quantifies the curvature concentrated on that hinge. The only upstream input is the RS time quantum τ₀ = 1 tick supplied by the Constants module, which sets the discrete time scale for the entire construction.

proof idea

This is a definition module. It introduces the types Simplex4D, Triangle, Tetrahedron, HingeData and the functions dihedral_from_cosine, deficit_angle, then records elementary facts such as flat_deficit_zero (zero deficit on flat lattices) and cubic_lattice_flat (right dihedral angles in the cubic case) together with the sign lemma deficit_pos_of_angle_deficit.

why it matters in Recognition Science

These definitions are imported directly by DiscreteBianchi, which encodes the discrete contracted Bianchi identity following Hamber and Kagel, and by NonlinearConvergence, which axiomatizes the Cheeger-Müller-Schrader theorem on convergence of the Regge action to the Einstein-Hilbert action at order a². The module therefore supplies the discrete geometry layer required to embed Recognition Science into the classical limit of general relativity.

scope and limits

Does not derive or vary the Regge action itself.
Does not prove the discrete Bianchi identity.
Does not contain any mesh-refinement or convergence estimates.
Does not import or use Recognition Science constants beyond τ₀.

used by (2)

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

IndisputableMonolith.Gravity.DiscreteBianchi module_import
IndisputableMonolith.Gravity.NonlinearConvergence module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (24)

structure Simplex4D L46
structure Triangle L51
structure Tetrahedron L69
structure DihedralAngleData L93
def dihedral_from_cosine L97
def cube_dihedral_angle L101
theorem cube_dihedral_is_right_angle L104
structure HingeData L115
def deficit_angle L121
theorem flat_deficit_zero L125
theorem cubic_lattice_flat L133
theorem deficit_pos_of_angle_deficit L137
theorem deficit_neg_of_angle_excess L143
def regge_action L159
theorem regge_action_flat L163
def regge_equations_statement L183
def schlafli_identity L191
def rs_edge_length L206
theorem rs_edge_length_pos L209
def rs_kappa L217
theorem rs_kappa_pos L219
theorem rs_kappa_value L222
structure ReggeCalculusCert L226
theorem regge_calculus_cert L237