module module

`IndisputableMonolith.Loom.Separation`

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

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

IndisputableMonolith.Gravity.Analysis.ClassicalSourceProjection module_import
IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4D module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Loom.CertificateData module_import
IndisputableMonolith.Loom.Grammar module_import
IndisputableMonolith.Loom.Readings module_import
IndisputableMonolith.Loom.Semantics module_import

declarations in this module (60)

def door L52
def key L53
def opens L54
def locks L55
def cb L62
def opensKeyDoor L64
def locksKeyDoor L65
def everyDoorSomeKeyOpens L68
def someKeyEveryDoorOpens L70
def everyDoorSomeKeyLocks L72
def someKeyEveryDoorLocks L74
def witnessA L77
def witnessB L79
theorem weave_witnessA L84
theorem weave_witnessB L85
theorem wellFormed_A L88
theorem wellFormed_B L90
theorem base_ok L100
theorem tableOfSubst_ok L105
theorem autSubst_length L109
theorem autTables_eq L114
theorem depth_one_is_blind L122
theorem abelianised_is_blind L127
theorem depth_two_separates L130
theorem invariant_separates L133
def gaugeImage L145
theorem invariant_gaugeImage L149
def separatesEverywhere L160
theorem separates_everywhere L163
theorem no_gauge_image_of_A_is_B L169
theorem gauge_image_ne_B L177
theorem witnesses_separated L185
def cb2 L216
def opensDoorKey L218
def locksDoorKey L219
def someDoorLocksEveryKey L222
def someDoorOpensEveryKey L224
def everyDoorOpensEveryKey L226
def everyDoorLocksEveryKey L228
def witnessC L230
def witnessD L231
theorem weave_witnessC L233
theorem weave_witnessD L234
theorem witnessC_ne_witnessD L238
def witnessModel L250
theorem witnessC_and_D_are_different_claims L259
theorem witnessC_holds L263
theorem witnessD_fails L264
theorem groundBag_blind L268
theorem adjacencyBag_blind L274
theorem depth_one_is_blind2 L279
theorem abelianised_is_blind2 L282
theorem depth_two_separates2 L285
theorem wellFormed_C L288
theorem wellFormed_D L290
def separatesEverywhere2 L293
theorem separates_everywhere2 L296
theorem no_gauge_image_of_C_is_D L301
theorem gauge_image_ne_D L308
theorem witnesses2_separated L313