module module

`IndisputableMonolith.Gravity.Analysis.ClassicalSourceProjection`

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.ClassicalSourceProjectionAudit module_import
IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4D module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Loom.Separation module_import

declarations in this module (15)

structure SourceProjection L47
def depthOneSource L54
def depthTwoReading L59
def abelianSource L63
def DepthOneProjection L67
def AbelianProjection L76
theorem depthOne_equal_cfgAB L87
theorem abelian_equal_cfgAB L93
theorem depthTwo_separates_cfgAB L99
theorem depthOne_equal_cfgCD L104
theorem abelian_equal_cfgCD L110
theorem depthTwo_separates_cfgCD L116
theorem decoy_depthOne_blind_on_discovery L122
theorem decoy_abelian_blind_on_discovery L127
theorem classicalEqual_recognitionUnequal_cfgAB L132