module module

`IndisputableMonolith.Gravity.DiscreteBianchi`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Gravity.ReggeCalculus module_import

declarations in this module (12)

structure HingeRotation L46
def compose_same_axis L51
def loop_holonomy L56
def discrete_bianchi_identity L78
def linearized_bianchi L83
theorem linearized_implies_general L87
theorem flat_bianchi L93
def discrete_conservation L118
theorem conservation_from_bianchi L125
def H_bianchi_continuum_limit L140
structure DiscreteBianchiCert L147
theorem discrete_bianchi_cert L154