IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4DAudit

   1import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
   2
   3/-!
   4# Axiom audit: `ReggeEdgeStencil4D`
   5
   6`#print axioms` for every public theorem of the 4D Regge edge-stencil /
   7provisional finite-quadratic layer.  Expected footprint:
   8`[propext, Classical.choice, Quot.sound]`.
   9-/
  10
  11open IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
  12
  13#print axioms classWeightNat_pos
  14#print axioms classDisp_ne_zero
  15#print axioms classDispSq_eq_weight
  16#print axioms classCoeff_add
  17#print axioms classCoeff_smul
  18#print axioms classCoeff_neg
  19#print axioms classCoeff_sub
  20#print axioms planeWaveClassPert_add
  21#print axioms planeWaveClassPert_smul
  22#print axioms finiteTTQuadratic_eq_bilinear
  23#print axioms finiteTTBilinear_symm
  24#print axioms finiteTTBilinear_add_left
  25#print axioms finiteTTBilinear_smul_left
  26#print axioms finiteTTQuadratic_add
  27#print axioms finiteTTQuadratic_smul
  28#print axioms finiteTTQuadratic_neg
  29#print axioms classCoeff_gaugePart
  30#print axioms finiteTTQuadratic_gaugePart
  31#print axioms classCoeff_gaugePart_axis
  32#print axioms sum_hasBit0
  33#print axioms finiteTTQuadratic_gaugePart_axisWave
  34#print axioms finiteTTQuadratic_gaugePart_axisWave_ne_zero
  35#print axioms classCoeff_axisTTPlus
  36#print axioms classCoeff_axisTTPlus_sq
  37#print axioms sum_axisTTPlusSqNat
  38#print axioms finiteTTQuadratic_axisTTPlus
  39#print axioms finiteTTQuadratic_axisTTPlus_ne_zero
  40#print axioms finiteTTQuadratic_axisTTPlus_isTT_seed
  41#print axioms sum_crossNat
  42#print axioms finiteTTBilinear_axisTTPlus_gauge
  43#print axioms finiteTTQuadratic_not_gauge_invariant_on_axisTTPlus
  44#print axioms finiteTTQuadratic_decoyGauge
  45#print axioms classCoeff_decoyTrace
  46#print axioms classCoeff_decoyTrace_sq
  47#print axioms sum_weightSqNat
  48#print axioms finiteTTQuadratic_decoyTrace
  49#print axioms decoy_values_distinct
  50#print axioms classDisp_axis0
  51#print axioms classCoeff_axis0
  52#print axioms planeWaveClassPert_axis0
  53