`IndisputableMonolith.Gravity.SevenGaps.WickActionCertFamilyAssemblyAudit`

IndisputableMonolith/Gravity/SevenGaps/WickActionCertFamilyAssemblyAudit.lean · 22 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.SevenGaps.WickActionCertFamilyAssembly
   2
   3/-!
   4# Axiom audit: Wave C4 F2 WickActionCertFamilyAssembly
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8Zero `sorryAx`.
   9-/
  10
  11open IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
  12
  13#check wickActionContinuationCertV2_of_causal
  14#check wick_action_continuation_4d_v2_holds
  15#check not_wick_action_continuation_4d
  16#check wick_action_continuation_v2_family_holds
  17
  18#print axioms wickActionContinuationCertV2_of_causal
  19#print axioms wick_action_continuation_4d_v2_holds
  20#print axioms not_wick_action_continuation_4d
  21#print axioms wick_action_continuation_v2_family_holds
  22

source mirrored from github.com/jonwashburn/shape-of-logic