module
module
IndisputableMonolith.Gravity.SevenGaps.WickActionCertFamilyAssembly
show as:
view Lean formalization →
used by (3)
depends on (2)
declarations in this module (8)
-
theorem
chartsAgree_of_causal -
theorem
euclidCosReal_of_causal -
theorem
euclidAnchor_of_causal -
theorem
wickActionContinuationCertV2_of_causal -
def
wick_action_continuation_4d_v2 -
theorem
wick_action_continuation_4d_v2_holds -
theorem
not_wick_action_continuation_4d -
theorem
wick_action_continuation_v2_family_holds