`IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4DAudit`

IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Symbol4DAudit.lean · 35 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
   2
   3/-!
   4# Axiom audit for `ReggeBlochM2Symbol4D`
   5
   6Every public theorem must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
  11
  12#print axioms classMidpointPhase_symbolDir
  13#print axioms phasedClassDot_symbolDir
  14#print axioms foldAlong_neg
  15#print axioms foldAlong_even
  16#print axioms foldAlong_odd_deriv_at_zero
  17#print axioms slotKerDotZ_axis
  18#print axioms slotKerDotZ_gauge
  19#print axioms classDot_slotDeficitKer_axis
  20#print axioms classDot_slotDeficitKer_gauge
  21#print axioms transportedSlotTerm_axis_zeroMomentum
  22#print axioms transportedSlotTerm_gauge_zeroMomentum
  23#print axioms foldAlong_axis_zero
  24#print axioms foldAlong_gauge_zero
  25#print axioms phaseScale_eq_phase2Nat
  26#print axioms m2SlotCoeff_eq_cert
  27#print axioms sum_m2SlotCertZ_axis
  28#print axioms sum_m2SlotCertZ_gauge
  29#print axioms m2Symbol_axisTTPlus
  30#print axioms m2Symbol_decoyGauge
  31#print axioms m2Symbol_axisTTPlus_ne_zero
  32#print axioms FoldAlongM2Tendsto_axis_iff
  33#print axioms FoldAlongM2Tendsto_gauge_iff
  34#print axioms blochM2Symbol4DStatus_flags
  35

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