/-
  StarG/Audit.lean, `#print axioms` audit of the main theorems.
  Building this file prints the full transitive axiom dependency of every
  named theorem; the manuscript claims exactly 5 axioms (matrix Eckart–Young,
  Parseval, Fourier multiplicative, Fourier injective, Fourier surjective)
  plus Lean's three built-in axioms (propext, Classical.choice, Quot.sound).
-/
import StarG.Algebra
import StarG.ProductGroup
import StarG.Equivariance
import StarG.SVD
import StarG.WignerEckart

open GroupTensor

#print axioms GroupTensor.starG_assoc
#print axioms GroupTensor.starG_identity_left
#print axioms GroupTensor.starG_identity_right
#print axioms GroupTensor.starG_add_left
#print axioms GroupTensor.starG_add_right
#print axioms GroupTensor.starG_transpose_mul
#print axioms GroupTensor.starG_equivariant_left
#print axioms GroupTensor.starG_equivariant_right
#print axioms GroupTensor.starG_prod_fourier      -- uses fourier_multiplicative
#print axioms GroupTensor.starG_svd_exists        -- uses fourier_injective + surjective
#print axioms GroupTensor.frobNormSq_invariant
#print axioms GroupTensor.fourier_power_invariant
#print axioms GroupTensor.eckart_young_starG      -- Theorem 1 of the paper
#print axioms GroupTensor.eckart_young_error
#print axioms GroupTensor.convTensor_prod         -- Theorem 2(ii) of the paper