`IndisputableMonolith.Gravity.Analysis.RecognitionMeshHingeKappa4DAudit`

IndisputableMonolith/Gravity/Analysis/RecognitionMeshHingeKappa4DAudit.lean · 30 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.RecognitionMeshHingeKappa4D
   2
   3/-!
   4# Axiom audit: RecognitionMeshHingeKappa4D (Wave B R2)
   5
   6Closure theorem and decoys must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.Analysis.RecognitionMeshHingeKappa4D
  11
  12#check TypedResidual_hinge_kappa_identified
  13#check typedResidual_hinge_kappa_identified_closed
  14#check meshHingeKappa
  15#check meshHingeKappa_source_dominated
  16#check decoy_zero_kappa_fails_nontrivial
  17#check decoy_log_ratio_over_deficit_ne_meshHingeKappa
  18#check adversarial_decoys_hinge_kappa
  19#check recognitionMeshHingeKappa4DStatus_flags
  20
  21#print axioms typedResidual_hinge_kappa_identified_closed
  22#print axioms TypedResidual_hinge_kappa_identified_closed
  23#print axioms meshHingeKappa_source_dominated
  24#print axioms meshGeometricDeficit_abs_le_two_pi
  25#print axioms abs_arcsin_le_pi_div_two
  26#print axioms decoy_zero_kappa_fails_nontrivial
  27#print axioms decoy_log_ratio_over_deficit_ne_meshHingeKappa
  28#print axioms adversarial_decoys_hinge_kappa
  29#print axioms recognitionMeshHingeKappa4DStatus_flags
  30

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