`IndisputableMonolith.Gravity.Analysis.ClassicalSourceProjectionAudit`

IndisputableMonolith/Gravity/Analysis/ClassicalSourceProjectionAudit.lean · 16 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ClassicalSourceProjection
   2
   3/-!
   4Axiom audit for ClassicalSourceProjection. Load-bearing theorems must report the
   5base triple `[propext, Classical.choice, Quot.sound]` (or a subset).
   6-/
   7
   8open IndisputableMonolith.Gravity.Analysis.ClassicalSourceProjection
   9
  10#print axioms depthOne_equal_cfgAB
  11#print axioms abelian_equal_cfgAB
  12#print axioms depthTwo_separates_cfgAB
  13#print axioms classicalEqual_recognitionUnequal_cfgAB
  14#print axioms decoy_depthOne_blind_on_discovery
  15#print axioms decoy_abelian_blind_on_discovery
  16

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