# ⋆_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](https://github.com/leanprover/elan) (the Lean version manager):

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

## Building

**Option A: Use the build script (recommended)**

```bash
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**

```bash
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:**
```bash
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 |