IndisputableMonolith.Gravity.Analysis.ReggeEdgeTTAttachment4DAudit

   1import IndisputableMonolith.Gravity.Analysis.ReggeEdgeTTAttachment4D
   2
   3/-!
   4# Axiom audit: `ReggeEdgeTTAttachment4D`
   5
   6`#print axioms` for every public theorem of the 4D Regge edge TT
   7attachment layer.  Expected footprint:
   8`[propext, Classical.choice, Quot.sound]`.
   9-/
  10
  11open IndisputableMonolith.Gravity.Analysis.ReggeEdgeTTAttachment4D
  12
  13#print axioms axisDisp_apply
  14#print axioms edgeLoad_axis
  15#print axioms edgeLoad_add
  16#print axioms edgeLoad_smul
  17#print axioms edgeLoad_neg
  18#print axioms edgeLoad_sub
  19#print axioms planeWaveAxisEdgePert_add
  20#print axioms planeWaveAxisEdgePert_smul
  21#print axioms edgeLoad_gaugePart
  22#print axioms edgeLoad_gaugePart_axis
  23#print axioms shiftAxis_dot
  24#print axioms sin_add_sub_sin
  25#print axioms discreteLieAxis_eq
  26#print axioms planeWaveAxisEdgePert_gaugePart
  27#print axioms planeWaveAxisEdgePert_gaugePart_eq_discreteLie
  28#print axioms edgeLoad_decomposition
  29#print axioms planeWaveAxisEdgePert_decomposition
  30#print axioms load_eq_zero_of_isTT
  31#print axioms gaugeVector_eq_zero_of_isTT
  32#print axioms gaugePart_zero
  33#print axioms gaugeCorrected_eq_of_isTT
  34#print axioms residualTrace_eq_zero_of_isTT
  35#print axioms ttProject_eq_of_isTT
  36#print axioms decoyTT_edgeLoad_axis2
  37#print axioms decoyTT_not_gaugeDiscreteLie_axis2
  38#print axioms decoyTT_isTT
  39#print axioms witness_isTT
  40#print axioms witness_momentumSq
  41#print axioms witness_ttProject_eq
  42#print axioms witness_edgeLoad_tt_ne_zero
  43#print axioms witness_tt_edge_ne_zero
  44