IndisputableMonolith.Gravity.Analysis.Regge4DAlgebraicCloserAudit

   1import IndisputableMonolith.Gravity.Analysis.Regge4DAlgebraicCloser
   2
   3/-!
   4Axiom / honesty audit for `Regge4DAlgebraicCloser`.
   5Expected footprint: `[propext, Classical.choice, Quot.sound]`.
   6-/
   7
   8namespace IndisputableMonolith
   9namespace Gravity
  10namespace Analysis
  11namespace Regge4DAlgebraicCloserAudit
  12
  13open Regge4DAlgebraicCloser
  14
  15#print axioms decoy_one_orbit_m2_ne_eh_coefficient
  16#print axioms plus_normalized_isTTPolarization
  17#print axioms cross_normalized_isTTPolarization
  18#print axioms tt_witnesses_nonvacuous
  19#print axioms gauge_m2Symbol_vanishes_on_decoy
  20#print axioms one_orbit_m2Symbol_axis_ne_zero
  21#print axioms eh_tt_coefficient_eq
  22#print axioms fullMomentZeroMomentum_eq_trueWeight
  23#print axioms fullMomentZeroMomentum_eq_bilinear
  24#print axioms fullMomentZeroMomentum_axisTTPlus
  25#print axioms fullMomentZeroMomentum_decoyGauge
  26#print axioms fullMomentZeroMomentum_decoyTrace
  27#print axioms fullMomentOrbitContribution_axisTTPlus
  28#print axioms fullMomentOrbitContribution_decoyGauge
  29#print axioms fullTTIsotropyTarget_mentions_eh_coefficient
  30#print axioms regge4DAlgebraicCloserStatus_flags
  31#print axioms banked_does_not_flip_gap_or_isotropy
  32
  33end Regge4DAlgebraicCloserAudit
  34end Analysis
  35end Gravity
  36end IndisputableMonolith
  37