module module

`IndisputableMonolith.Gravity.ReggeCalculus`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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