module module high

`IndisputableMonolith.Gravity.ReggeCalculus`

ReggeCalculus supplies the core geometric primitives for 4D Regge calculus: 4-simplices fixed by ten edge lengths, triangles, tetrahedra, dihedral angles, and deficit angles. Workers on discrete gravity models cite these definitions when building lattice approximations to general relativity. The module is purely definitional, establishing basic relations such as flat deficit zero without deeper theorems.

claimA $4$-simplex has five vertices and ten edges whose lengths fix the geometry. Dihedral angles are obtained from edge lengths via the cosine law; deficit angles measure curvature at hinges. Flat configurations satisfy zero deficit.

background

The module imports Constants, where the RS time quantum satisfies $\tau_0 = 1$ tick. It introduces Simplex4D as the $4$-simplex with five vertices and $\binom{5}{2}=10$ edges, together with Triangle, Tetrahedron, HingeData, dihedral_from_cosine, deficit_angle, and flat_deficit_zero. These objects encode the discrete geometry of Regge calculus inside the Recognition Science framework.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed DiscreteBianchi, which formalizes the discrete Bianchi identity following Hamber and Kagel, and NonlinearConvergence, which axiomatizes the Cheeger-Müller-Schrader convergence of the Regge action to the Einstein-Hilbert action at $O(a^2)$. It supplies the simplicial building blocks required by both downstream results.

scope and limits

Does not derive the Einstein field equations from the Regge action.
Does not treat quantum gravity or path-integral measures.
Does not include numerical mesh refinement algorithms.
Does not cover simplices in dimensions other than four.

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