IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionLorentz4DAudit

   1import IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionLorentz4D
   2
   3/-!
   4# Axiom audit: `EdgeTTDecompositionLorentz4D`
   5
   6`#print axioms` for every public theorem of the Lorentzian algebraic 4D TT
   7decomposition layer.  Expected footprint:
   8`[propext, Classical.choice, Quot.sound]`.
   9-/
  10
  11open IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionLorentz4D
  12
  13#print axioms lorentzLoad_eq
  14#print axioms IsLorentzTransverse_iff_lorentzLoad
  15#print axioms minkowskiDot_eq_sum
  16#print axioms minkowskiDot_comm
  17#print axioms minkowskiTrace_eq_sum
  18#print axioms gaugePart_symmetric
  19#print axioms outerSq_symmetric
  20#print axioms symmetrizedOuter_symmetric
  21#print axioms raise_raise
  22#print axioms lorentzLoad_smul
  23#print axioms lorentzLoad_sub
  24#print axioms lorentzLoad_eta
  25#print axioms lorentzLoad_outerSq
  26#print axioms lorentzLoad_symmetrizedOuter
  27#print axioms lorentzLoad_symmetrizedOuter_l
  28#print axioms lorentzLoad_gaugePart
  29#print axioms minkowskiTrace_smul
  30#print axioms minkowskiTrace_sub
  31#print axioms minkowskiTrace_add
  32#print axioms minkowskiTrace_eta
  33#print axioms minkowskiTrace_outerSq
  34#print axioms minkowskiTrace_symmetrizedOuter
  35#print axioms minkowskiDot_eq_MinkowskiNull
  36#print axioms minkowskiEta_symmetric
  37#print axioms transverseProjector_symmetric
  38#print axioms lorentzLoad_transverseProjector
  39#print axioms minkowskiDot_gaugeVector
  40#print axioms lorentzLoad_gaugePart_gaugeVector
  41#print axioms gaugeCorrected_transverse
  42#print axioms gaugeCorrected_symmetric
  43#print axioms minkowskiTrace_transverseProjector
  44#print axioms ttProject_symmetric
  45#print axioms ttProject_transverse
  46#print axioms ttProject_traceless
  47#print axioms ttProject_isLorentzTT
  48#print axioms exists_lorentzTTDecomposition
  49#print axioms exists_lorentzTTDecomposition'
  50#print axioms nullProjector_symmetric
  51#print axioms nullProjector_minkowskiTrace
  52#print axioms lorentzLoad_nullProjector_m
  53#print axioms lorentzLoad_nullProjector_l
  54#print axioms sum_kron_left
  55#print axioms sum_kron_right
  56#print axioms nullPhp_expand_algebra
  57#print axioms sum_kron_H_kron
  58#print axioms sum_S_H_kron
  59#print axioms sum_kron_H_S
  60#print axioms nullPhp_entry
  61#print axioms sum_nullSMixed_H_col
  62#print axioms sum_H_nullSMixed_row
  63#print axioms nullGap_entry
  64#print axioms null_gap_expansion
  65#print axioms nullPhp_symmetric
  66#print axioms sum_nullSMixed_raise_m
  67#print axioms sum_nullPMixed_raise_m
  68#print axioms sum_nullSMixed_raise_l
  69#print axioms sum_nullPMixed_raise_l
  70#print axioms nullPhp_lorentzLoad_m
  71#print axioms nullPhp_transverse_m
  72#print axioms nullPhp_lorentzLoad_l
  73#print axioms nullPhp_transverse_l
  74#print axioms nullTTProject_symmetric
  75#print axioms nullTTProject_traceless
  76#print axioms nullTTProject_transverse_m
  77#print axioms nullTTProject_transverse_l
  78#print axioms nullTTProject_isLorentzTT
  79#print axioms exists_nullLorentzTTDecomposition
  80#print axioms nullAxisWave_dot
  81#print axioms nullAxisAux_dot
  82#print axioms nullAxis_cross_dot
  83#print axioms nullAxisWave_ne_zero
  84#print axioms nullAxis_MinkowskiNull
  85#print axioms nullAxisTTPlus_isLorentzTT
  86#print axioms nullAxisTTCross_isLorentzTT
  87#print axioms nullAxisTTPlus_ne_zero
  88#print axioms nullAxisTTCross_ne_zero
  89#print axioms nullAxisTT_independent
  90#print axioms nullAxis_euclideanMomentumSq
  91#print axioms lorentzLoad_one
  92#print axioms euclideanProjector_not_lorentzTransverse_on_nullAxis
  93#print axioms naive_lorentz_projector_hypothesis_fails_on_nullAxis
  94#print axioms zero_wave_minkowskiDot
  95#print axioms decomposition_hypothesis_fails_at_zero
  96