module module

`IndisputableMonolith.Gravity.Analysis.FoldMomentNamingLink4D`

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

declarations in this module (11)

def hybridT11Provenance L47
def foldT11Provenance L50
theorem t11_provenance_mismatch L54
theorem witness_factor_two_is_not_naming_link L60
def namingLinkClosedAsDefinition L66
theorem namingLinkClosedAsDefinition_eq L68
def namingLinkClosedAtWitnesses L73
theorem namingLinkClosedAtWitnesses_eq L75
def namingLinkClosed L79
theorem namingLinkClosed_eq L81
theorem step9_task1_status L85