module module

`IndisputableMonolith.Gravity.DiscreteCurvature`

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 (1)

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

IndisputableMonolith.Gravity.LatticeRicci module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (17)

def cube_dihedral L56
def cubes_per_edge L59
def deficit_angle_flat L63
theorem flat_deficit_zero L65
def deficit_angle_deformed L75
theorem deficit_zero_when_flat L79
theorem deficit_scales_with_a_squared L83
def curvature_from_deficit L92
theorem curvature_equals_d2h L98
def linearized_ricci_from_deficits L113
theorem ricci_is_sum_of_curvatures L116
def vertex_deficit_cube L133
theorem vertex_deficit_value L135
theorem gauss_bonnet_cube L138
theorem euler_characteristic_from_deficit L143
structure DiscreteCurvatureCert L151
theorem discrete_curvature_cert L158