module module

`IndisputableMonolith.Gravity.Analysis.ContinuumOrderSensitiveResidual4D`

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.Analysis.OrderSensitiveCoefficientForce4D module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.MetricEdgeImage4D module_import
IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4D module_import
IndisputableMonolith.Loom.CertificateData module_import

declarations in this module (14)

def edgeNorm L50
structure RefinementFamily L54
def normalizedSeparation L61
def Survives L67
def MetricCollapse L72
def LatticeWashout L77
theorem finite_outside_metric_image L81
theorem collapse_not_washout L86
def ContinuumSurvivalOpen L91
def ContinuumMetricCollapseOpen L95
def ContinuumWashoutOpen L99
def continuumPromotionEarned L103
theorem continuumPromotionEarned_eq L105
theorem finite_exclusion_does_not_earn_promotion L110