module module

`IndisputableMonolith.Foundation.ContinuumLimit`

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

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

IndisputableMonolith.Gravity.ContinuumManifoldEmergence module_import
IndisputableMonolith.Gravity.CubicReggeConvergence module_import
IndisputableMonolith.Gravity.CubicReggeProof module_import
IndisputableMonolith.Gravity.LatticeConvergence module_import
IndisputableMonolith.Gravity.ReggeConvergence module_import
IndisputableMonolith.Gravity.UnifiedLatticeManifoldCorrespondence module_import

depends on (8)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.Convexity module_import
IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.Foundation.InitialCondition module_import
IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.Foundation.Thermodynamics module_import
IndisputableMonolith.Foundation.VariationalDynamics module_import

declarations in this module (32)

theorem jcost_quadratic_leading L68
def quadratic_cost L73
theorem quadratic_approximates_jlog L76
theorem relative_error_vanishes L84
def LatticeField L101
def shift_plus L104
def shift_minus L107
def lattice_laplacian L114
theorem lattice_laplacian_const L119
theorem lattice_laplacian_add L126
theorem lattice_laplacian_smul L133
def neighbor_cost L145
theorem jcost_gives_laplacian_structure L163
def lattice_spacing L214
theorem fourth_deriv_continuous L227
def fourthDerivBound L233
theorem le_fourthDerivBound L237
theorem fourthDerivBound_nonneg L244
theorem continuum_limit_second_order L262
structure GaussianUniversality L477
theorem rs_is_gaussian L484
def kg_mass_squared L497
theorem mass_from_curvature L500
structure KleinGordonStructure L515
def rs_klein_gordon L522
inductive EmergenceLevel L542
def emergence_error L549
theorem emergence_hierarchy L556
theorem jcost_fixes_universality L594
structure LatticeToContDict L607
def continuum_dictionary L611
theorem continuum_limit_certificate L654