IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4DAudit

   1import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   2
   3/-!
   4# Axiom audit: `EdgeTTDecomposition4D`
   5
   6`#print axioms` for every public theorem of the algebraic 4D TT
   7decomposition layer.  Expected footprint:
   8`[propext, Classical.choice, Quot.sound]`.
   9-/
  10
  11open IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
  12
  13#print axioms gaugePart_symmetric
  14#print axioms outerSq_symmetric
  15#print axioms transverseProjector_symmetric
  16#print axioms load_gaugePart
  17#print axioms load_smul
  18#print axioms load_sub
  19#print axioms load_one
  20#print axioms load_outerSq
  21#print axioms load_transverseProjector
  22#print axioms dot_gaugeVector
  23#print axioms load_gaugePart_gaugeVector
  24#print axioms gaugeCorrected_transverse
  25#print axioms gaugeCorrected_symmetric
  26#print axioms euclideanTrace_smul
  27#print axioms euclideanTrace_sub
  28#print axioms euclideanTrace_one
  29#print axioms euclideanTrace_outerSq
  30#print axioms euclideanTrace_transverseProjector
  31#print axioms ttProject_symmetric
  32#print axioms ttProject_transverse
  33#print axioms ttProject_traceless
  34#print axioms ttProject_isTT
  35#print axioms exists_edgeTTDecomposition
  36#print axioms exists_edgeTTDecomposition'
  37#print axioms axisWave_momentumSq
  38#print axioms axisTTPlus_isTT
  39#print axioms axisTTCross_isTT
  40#print axioms axisTTPlus_ne_zero
  41#print axioms axisTTCross_ne_zero
  42#print axioms axisTT_independent
  43#print axioms decoyLongitudinal_symmetric
  44#print axioms decoyLongitudinal_not_transverse
  45#print axioms decoy_ttProject_isTT
  46#print axioms decoy_projection_restores_transverse
  47#print axioms zero_wave_momentumSq
  48#print axioms decomposition_hypothesis_fails_at_zero
  49