module module high

`IndisputableMonolith.Gravity.ReggeCalculus`

The ReggeCalculus module supplies the combinatorial and geometric primitives for 4-dimensional simplicial gravity within Recognition Science. It encodes 4-simplices by their 10 edge lengths and defines dihedral and deficit angles. Researchers working on discrete approximations to Einstein gravity would cite these definitions when building Bianchi identities or convergence results. The module is purely definitional, establishing the basic objects and some elementary relations such as zero deficit in flat lattices.

claimA 4-simplex $\sigma^4$ is specified by 10 edge lengths $\ell_{ij}$ ($1\leq i<j\leq5$). Dihedral angles at hinges are obtained from the cosine law on adjacent triangles; the deficit angle at an edge is $\delta=2\pi-\sum\theta_i$.

background

This module operates in the discrete gravity sector of Recognition Science, building on the RS time quantum $\tau_0=1$ from Constants. It introduces Simplex4D as a 4-simplex with five vertices whose geometry is fixed by the ten edge lengths, per the module doc-comment. Triangle and Tetrahedron provide the lower-dimensional building blocks. DihedralAngleData and deficit_angle capture the curvature via angle deficits at hinges, with lemmas such as flat_deficit_zero showing vanishing curvature in cubic lattices.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module provides the foundational objects for the discrete Bianchi identity formalized in DiscreteBianchi and the convergence of the Regge action to the Einstein-Hilbert action in NonlinearConvergence. It fills the role of supplying the Regge calculus primitives needed to discretize the contracted Bianchi identity $\nabla^\mu G_{\mu\nu}=0$ and to state the Cheeger-Müller-Schrader theorem in the RS setting.

scope and limits

Does not address the continuum limit or mesh refinement.
Does not incorporate matter couplings or sources.
Does not derive the Regge action itself.
Does not prove the discrete Bianchi identity.

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