`IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioDerivedAudit`

IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioDerivedAudit.lean · 21 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioDerived
   2
   3/-!
   4# Axiom audit: Wave B R5 ledger-named `recognition_ratio_derived`
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps
  11
  12#check recognition_ratio_derived
  13#check recognition_ratio_derived_holds
  14#check typedResidual_recognition_ratio_derived_closed
  15#check recognitionRatioDerivedStatus_flags
  16
  17#print axioms recognition_ratio_derived_holds
  18#print axioms typedResidual_recognition_ratio_derived_closed
  19#print axioms TypedResidual_recognition_ratio_derived_closed
  20#print axioms recognitionRatioDerivedStatus_flags
  21

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