/-
  StarG.lean
  Root module for the ⋆_G tensor algebra formalization.

  Formalizes the proofs from:
    "Group-Algebraic Tensors: Optimal Equivariant Learning
     and Physical Symmetry Discovery"
    Hoyos, Ubaru, Huh, Kalantzis, Clarkson, Kilmer, Avron, Horesh

  Structure:
    Basic.lean         Core definitions (convolution tensor, ⋆_G product, transpose)
    Algebra.lean       Algebraic properties (associativity, identity, distributivity)
    SVD.lean           ⋆_G-SVD and Eckart-Young optimality (Theorem 1)
    ProductGroup.lean  Product group composition (Theorem 2)
    Equivariance.lean  Equivariance and feature invariance (SI §7)
    WignerEckart.lean  Selection rules for the octahedral group (§2.5)
-/
import StarG.Basic
import StarG.Algebra
import StarG.SVD
import StarG.ProductGroup
import StarG.Equivariance
import StarG.WignerEckart