module module

`IndisputableMonolith.Gravity.ReggeConvergenceRegistry`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.NonlinearConvergence module_import

declarations in this module (13)

structure ReggeConvergenceRegistry L48
theorem cms_measure_bound_faithful L69
theorem special_quadratic_faithful L74
theorem ricci_convergence_faithful L79
theorem riemann_convergence_faithful L84
def mk L93
theorem mk_cms_measure_bound L106
theorem mk_special_quadratic L116
theorem mk_ricci_convergence L126
theorem mk_riemann_convergence L136
theorem mk_provenance L146
theorem mk_roundtrip L158
def defaultProvenance L166