feat: Add spectral analysis module with Atlas λ₁=1 proof

.github/workflows/ci.yml

@@ -0,0 +1,125 @@
+name: CI
+
+on:
+  push:
+    branches: [ main, develop ]
+    paths:
+      - 'atlas-embeddings/**'
+      - '.github/workflows/ci.yml'
+  pull_request:
+    branches: [ main, develop ]
+    paths:
+      - 'atlas-embeddings/**'
+      - '.github/workflows/ci.yml'
+
+env:
+  CARGO_TERM_COLOR: always
+  RUSTFLAGS: -D warnings
+
+jobs:
+  check:
+    name: Check
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: atlas-embeddings
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+      - uses: Swatinem/rust-cache@v2
+        with:
+          workspaces: atlas-embeddings
+      - run: cargo check --all-features
+      - run: cargo check --no-default-features
+
+  test:
+    name: Test Suite
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        working-directory: atlas-embeddings
+    strategy:
+      matrix:
+        os: [ubuntu-latest, windows-latest, macos-latest]
+        rust: [stable, beta]
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: ${{ matrix.rust }}
+      - uses: Swatinem/rust-cache@v2
+        with:
+          workspaces: atlas-embeddings
+      - run: cargo test --all-features
+
+  fmt:
+    name: Rustfmt
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: atlas-embeddings
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: rustfmt
+      - run: cargo fmt --all -- --check
+
+  clippy:
+    name: Clippy
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: atlas-embeddings
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: clippy
+      - uses: Swatinem/rust-cache@v2
+        with:
+          workspaces: atlas-embeddings
+      - run: cargo clippy --all-targets --all-features -- -D warnings -D clippy::all -D clippy::pedantic -D clippy::nursery -D clippy::cargo -D clippy::float_arithmetic
+
+  docs:
+    name: Documentation
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: atlas-embeddings
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+      - uses: Swatinem/rust-cache@v2
+        with:
+          workspaces: atlas-embeddings
+      - run: cargo doc --all-features --no-deps
+        env:
+          RUSTDOCFLAGS: -D warnings
+
+  audit:
+    name: Security Audit
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: atlas-embeddings
+    steps:
+      - uses: actions/checkout@v4
+      - uses: rustsec/audit-check@v1.4.1
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+
+  benchmarks:
+    name: Benchmarks
+    runs-on: ubuntu-latest
+    if: github.event_name == 'pull_request'
+    defaults:
+      run:
+        working-directory: atlas-embeddings
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+      - uses: Swatinem/rust-cache@v2
+        with:
+          workspaces: atlas-embeddings
+      - run: cargo bench --all-features --no-fail-fast

.github/workflows/docs.yml

@@ -0,0 +1,56 @@
+name: Documentation
+
+on:
+  push:
+    branches: [ main ]
+    paths:
+      - 'atlas-embeddings/**'
+      - '.github/workflows/docs.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: false
+
+jobs:
+  build:
+    name: Build Documentation
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: dtolnay/rust-toolchain@stable
+
+      - uses: Swatinem/rust-cache@v2
+        with:
+          workspaces: atlas-embeddings
+
+      - name: Build documentation
+        working-directory: atlas-embeddings
+        run: |
+          cargo doc --all-features --no-deps
+          echo '<meta http-equiv="refresh" content="0; url=atlas_embeddings/">' > target/doc/index.html
+        env:
+          RUSTDOCFLAGS: --html-in-header docs/katex-header.html
+
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: atlas-embeddings/target/doc
+
+  deploy:
+    name: Deploy to GitHub Pages
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: build
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4

.github/workflows/lean4.yml

@@ -0,0 +1,153 @@
+name: Lean 4
+
+on:
+  push:
+    branches: [ main, develop ]
+    paths:
+      - 'atlas-embeddings/lean4/**'
+      - '.github/workflows/lean4.yml'
+  pull_request:
+    branches: [ main, develop ]
+    paths:
+      - 'atlas-embeddings/lean4/**'
+      - '.github/workflows/lean4.yml'
+
+jobs:
+  build:
+    name: Build and Verify
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Install Elan (Lean version manager)
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Cache mathlib4
+        uses: actions/cache@v4
+        with:
+          path: |
+            atlas-embeddings/lean4/.lake
+            atlas-embeddings/lean4/lake-packages
+          key: ${{ runner.os }}-lean4-${{ hashFiles('atlas-embeddings/lean4/lean-toolchain', 'atlas-embeddings/lean4/lakefile.lean') }}
+          restore-keys: |
+            ${{ runner.os }}-lean4-
+
+      - name: Update Lake dependencies
+        working-directory: atlas-embeddings/lean4
+        run: lake update
+
+      - name: Download mathlib4 cache
+        working-directory: atlas-embeddings/lean4
+        run: lake exe cache get || true
+
+      - name: Build Lean project
+        working-directory: atlas-embeddings/lean4
+        run: lake build
+
+      - name: Verify no sorry statements
+        working-directory: atlas-embeddings/lean4
+        run: |
+          # Look for actual sorry usage (not in comments)
+          # Match: sorry, sorry), := sorry, etc. but not "NO `sorry` POLICY"
+          if grep -rE '\bsorry\b' AtlasEmbeddings/ --include="*.lean" | grep -v "^\-\-" | grep -v "NO.*sorry.*POLICY" | grep -v "ZERO sorrys"; then
+            echo "Error: Found 'sorry' statements in Lean code"
+            echo "All theorems must be fully proven (NO sorry POLICY)"
+            exit 1
+          else
+            echo "Success: No 'sorry' statements found in code"
+          fi
+
+      - name: Count theorems
+        working-directory: atlas-embeddings/lean4
+        run: |
+          THEOREM_COUNT=$(grep -r "^theorem " AtlasEmbeddings/ --include="*.lean" | wc -l)
+          echo "Total theorems proven: $THEOREM_COUNT"
+          if [ "$THEOREM_COUNT" -lt 30 ]; then
+            echo "Warning: Expected at least 30 theorems, found $THEOREM_COUNT"
+          fi
+
+  test:
+    name: Run Lean Tests
+    runs-on: ubuntu-latest
+    needs: build
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Install Elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Cache mathlib4
+        uses: actions/cache@v4
+        with:
+          path: |
+            atlas-embeddings/lean4/.lake
+            atlas-embeddings/lean4/lake-packages
+          key: ${{ runner.os }}-lean4-${{ hashFiles('atlas-embeddings/lean4/lean-toolchain', 'atlas-embeddings/lean4/lakefile.lean') }}
+          restore-keys: |
+            ${{ runner.os }}-lean4-
+
+      - name: Update Lake dependencies
+        working-directory: atlas-embeddings/lean4
+        run: lake update
+
+      - name: Download mathlib4 cache
+        working-directory: atlas-embeddings/lean4
+        run: lake exe cache get || true
+
+      - name: Test individual modules
+        working-directory: atlas-embeddings/lean4
+        run: |
+          echo "Testing Arithmetic module..."
+          lake env lean AtlasEmbeddings/Arithmetic.lean
+
+          echo "Testing E8 module..."
+          lake env lean AtlasEmbeddings/E8.lean
+
+          echo "Testing Atlas module..."
+          lake env lean AtlasEmbeddings/Atlas.lean
+
+          echo "Testing Embedding module..."
+          lake env lean AtlasEmbeddings/Embedding.lean
+
+          echo "Testing Groups module..."
+          lake env lean AtlasEmbeddings/Groups.lean
+
+          echo "Testing ActionFunctional module..."
+          lake env lean AtlasEmbeddings/ActionFunctional.lean
+
+          echo "Testing Completeness module..."
+          lake env lean AtlasEmbeddings/Completeness.lean
+
+  formatting:
+    name: Check Formatting
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Check line length
+        working-directory: atlas-embeddings/lean4
+        run: |
+          if grep -rn ".\{101,\}" AtlasEmbeddings/ --include="*.lean" | grep -v "http"; then
+            echo "Warning: Found lines longer than 100 characters"
+            echo "Consider breaking long lines for readability"
+            exit 0
+          else
+            echo "Success: All lines are 100 characters or less"
+          fi
+
+      - name: Check for tabs
+        working-directory: atlas-embeddings/lean4
+        run: |
+          if grep -r $'\t' AtlasEmbeddings/ --include="*.lean"; then
+            echo "Error: Found tab characters (use spaces)"
+            exit 1
+          else
+            echo "Success: No tab characters found"
+          fi