module module

`IndisputableMonolith.Gravity.CubicReggeConvergence`

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.ReggeCubicLatticeLimit module_import

depends on (6)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.ContinuumLimit module_import
IndisputableMonolith.Foundation.GrowthBounds module_import
IndisputableMonolith.Gravity.NonlinearConvergence module_import
IndisputableMonolith.Gravity.ReggeCalculus module_import
IndisputableMonolith.Gravity.ReggeConvergence module_import

declarations in this module (15)

def rs_lattice_action L67
def continuum_action L71
theorem quartic_error_controlled L84
theorem weak_field_error_estimate L91
structure WeakFieldConvergence L107
def weak_field_convergence L121
structure RSCubicConvergenceConditions L148
theorem rs_cubic_shape_quality L155
def rs_convergence_bound L162
def uv_cutoff L177
theorem uv_cutoff_pos L180
theorem phi_exponential_growth L192
theorem exponential_defeats_cubic L197
structure CubicConvergenceCert L207
theorem cubic_convergence_cert L216