⋆_G Tensor Algebra: Lean 4 Formalization

Lean 4 + Mathlib formalization of the proofs from:

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

Status

0 sorry across all 6 modules (600 lines total)
5 axioms, all standard textbook results not yet in Mathlib

Prerequisites

Install elan (the Lean version manager):

curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
source ~/.profile

Building

Option A: Use the build script (recommended)

cd starG-lean
./build.sh

This automatically fetches Mathlib, syncs the Lean toolchain version, downloads prebuilt caches, and builds the project.

Option B: Manual steps

cd starG-lean

# 1. Fetch Mathlib
lake update

# 2. IMPORTANT: Sync toolchain to match Mathlib's requirement.
#    Without this step you will get version mismatch errors.
cp .lake/packages/mathlib/lean-toolchain ./lean-toolchain

# 3. Download prebuilt Mathlib .olean files (avoids multi-hour rebuild)
lake exe cache get

# 4. Build
lake build

Troubleshooting

"unknown module prefix 'Mathlib'", You need to run lake update first. Mathlib is not bundled; it is fetched from GitHub.

"no such file or directory ... Mathlib/...", Toolchain version mismatch. Run: cp .lake/packages/mathlib/lean-toolchain ./lean-toolchain then: lake exe cache get && lake build

"toolchain 'leanprover/lean4:vX.Y.Z' is not installed", elan will auto-install it. Just run the command again.

Starting fresh:

rm -rf .lake lake-packages
./build.sh

Architecture

File	Lines	Paper Section
`Basic.lean`	109	SI 1-4: convolution tensor, star product, transpose, identity
`Algebra.lean`	135	SI 4: associativity, distributivity, identity, transpose
`ProductGroup.lean`	137	Theorem 2: product group factorization, Kronecker irreps
`Equivariance.lean`	146	SI 7: equivariance, Frobenius/Fourier power invariance
`WignerEckart.lean`	155	2.5: octahedral irreps, CG multiplicities, selection rules
`SVD.lean`	215	Theorem 1: SVD existence, Eckart-Young optimality

Axioms (5, all in SVD.lean)

#	Axiom	Reference
1	`matrix_best_rank_k_approx`	Eckart and Young 1936
2	`parseval_group`	Serre, Linear Reps of Finite Groups, 2.4
3	`fourier_multiplicative`	Terras, Fourier Analysis on Finite Groups, Ch. 7
4	`fourier_injective`	Peter-Weyl completeness
5	`fourier_surjective`	Peter-Weyl + Fourier inversion