Refactor/lean4 standard structure

.github/workflows/blueprint.yml

@@ -5,17 +5,16 @@ on:
     branches:
       - main
     paths:
-      - "Lean/**/*.lean"
+      - "GIFT/**/*.lean"
       - "lean-toolchain"
-      - "lakefile.toml"
-      - "lake-manifest.json"
+      - "lakefile.lean"
       - "blueprint/**"
-      - "home_page/**"
+      - "contrib/homepage/**"
   pull_request:
     branches:
       - main
     paths:
-      - "Lean/**/*.lean"
+      - "GIFT/**/*.lean"
       - "blueprint/**"
   workflow_dispatch:
 
@@ -68,16 +67,16 @@ jobs:
             sleep $((i * 10))
           done
 
-      - name: Check for home_page folder
-        id: check_home_page
+      - name: Check for homepage folder
+        id: check_homepage
         run: |
-          if [ -d home_page ]; then
+          if [ -d contrib/homepage ]; then
             echo "exists=true" >> "$GITHUB_OUTPUT"
           else
             echo "exists=false" >> "$GITHUB_OUTPUT"
           fi
 
-      - name: Build blueprint and copy to home_page/blueprint
+      - name: Build blueprint and copy to homepage
         uses: xu-cheng/texlive-action@v2
         with:
           docker_image: ghcr.io/xu-cheng/texlive-full:20250101
@@ -95,42 +94,42 @@ jobs:
             pip install leanblueprint
             cd $GITHUB_WORKSPACE
             leanblueprint pdf
-            mkdir -p home_page
-            cp blueprint/print/print.pdf home_page/blueprint.pdf
+            mkdir -p contrib/homepage
+            cp blueprint/print/print.pdf contrib/homepage/blueprint.pdf
             leanblueprint web
             python3 blueprint/src/postprocess.py
-            cp -r blueprint/web home_page/blueprint
+            cp -r blueprint/web contrib/homepage/blueprint
 
       - name: Check declarations in blueprint exist in Lean
         run: |
           ~/.elan/bin/lake exe checkdecls blueprint/lean_decls || echo "Warning: Some declarations not found"
 
       - name: Setup Ruby
-        if: ${{ steps.check_home_page.outputs.exists == 'true' }}
+        if: ${{ steps.check_homepage.outputs.exists == 'true' }}
         uses: ruby/setup-ruby@v1
         with:
           ruby-version: '3.2'
           bundler-cache: false
 
       - name: Build Jekyll site
-        if: ${{ steps.check_home_page.outputs.exists == 'true' }}
+        if: ${{ steps.check_homepage.outputs.exists == 'true' }}
         run: |
-          cd home_page
+          cd contrib/homepage
           rm -f Gemfile.lock || true
           bundle config set --local path vendor/bundle
           bundle install --jobs 4 --retry 3
-          JEKYLL_ENV=production bundle exec jekyll build -d ../.jekyll-out/site
+          JEKYLL_ENV=production bundle exec jekyll build -d ../../.jekyll-out/site
 
       - name: Prepare Pages artifact (with Jekyll)
-        if: ${{ steps.check_home_page.outputs.exists == 'true' }}
+        if: ${{ steps.check_homepage.outputs.exists == 'true' }}
         run: |
           ls -la .jekyll-out/site || true
 
       - name: Prepare Pages artifact (without Jekyll)
-        if: ${{ steps.check_home_page.outputs.exists == 'false' }}
+        if: ${{ steps.check_homepage.outputs.exists == 'false' }}
         run: |
           mkdir -p .jekyll-out/site
-          cp -r home_page/* .jekyll-out/site/ || true
+          cp -r contrib/homepage/* .jekyll-out/site/ || true
 
       - name: Upload Pages artifact
         if: github.ref == 'refs/heads/main'

.github/workflows/publish.yml

@@ -27,7 +27,10 @@ jobs:
       - name: Build
         run: |
           pip install build
+          cd contrib/python
           python -m build
 
       - name: Publish to PyPI
         uses: pypa/gh-action-pypi-publish@release/v1
+        with:
+          packages-dir: contrib/python/dist/

.github/workflows/verify.yml

@@ -3,7 +3,7 @@ name: Formal Verification
 on:
   push:
     branches: [main]
-    paths: ['Lean/**']
+    paths: ['GIFT/**', 'GIFTTest/**', 'lakefile.lean', 'lean-toolchain']
   pull_request:
     branches: [main]
   workflow_dispatch:
@@ -13,9 +13,6 @@ jobs:
   lean:
     name: Lean 4 Verification
     runs-on: ubuntu-latest
-    defaults:
-      run:
-        working-directory: Lean
     steps:
       - uses: actions/checkout@v4
 
@@ -27,8 +24,8 @@ jobs:
       - name: Cache .lake
         uses: actions/cache@v4
         with:
-          path: Lean/.lake
-          key: lean-${{ hashFiles('Lean/lakefile.toml') }}
+          path: .lake
+          key: lean-${{ hashFiles('lakefile.lean') }}
 
       - name: Build
         run: |
@@ -38,11 +35,7 @@ jobs:
 
       - name: Verify zero sorry
         run: |
-          if grep -r "sorry" GIFT/ --include="*.lean"; then
+          if grep -r "sorry" GIFT/ GIFTTest/ --include="*.lean"; then
             echo "ERROR: Found sorry!"
             exit 1
           fi
-
-  # NOTE: Coq verification removed in v3.3.14
-  # Coq code removed in v3.3.25 (was archived, 75 relations, arithmetic-only proofs)
-  # Lean 4 is the sole proof assistant (455+ relations, real mathematics via Mathlib)

.gitignore

@@ -40,37 +40,24 @@ ENV/
 htmlcov/
 .pytest_cache/
 .hypothesis/
+tests/
 
 # Lean
 .lake/
-Lean/.lake/
-Lean/lake-packages/
-Lean/build/
-lake-manifest.json
-
-# Coq
-COQ/*.vo
-COQ/*.vok
-COQ/*.vos
-COQ/*.glob
-COQ/.*.aux
-COQ/CoqMakefile
-COQ/CoqMakefile.conf
-COQ/.coqdeps.d
 
 # Blueprint (generated)
 blueprint/web/
 blueprint/print/
-home_page/blueprint/
-home_page/blueprint.pdf
-home_page/docs/
+contrib/homepage/blueprint/
+contrib/homepage/blueprint.pdf
+contrib/homepage/docs/
 .jekyll-out/
 
 # Jekyll
-home_page/_site/
-home_page/.sass-cache/
-home_page/.jekyll-cache/
-home_page/Gemfile.lock
+contrib/homepage/_site/
+contrib/homepage/.sass-cache/
+contrib/homepage/.jekyll-cache/
+contrib/homepage/Gemfile.lock
 
 # OS
 .DS_Store

Lean/GIFT.lean → GIFT.lean

@@ -1,6 +1,6 @@
 -- GIFT: Geometric Integration of Fundamental Topologies
 -- Main entry point for Lean 4 formalization
--- Version: 3.3.47 (460+ certified relations, 11 published axioms)
+-- Version: 3.4.0 (460+ certified relations, 11 published axioms)
 
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- CORE & RELATIONS

Lean/GIFT/Test/AristotleSpectrumCountableTest.lean → GIFTTest/AristotleSpectrumCountableTest.lean

@@ -56,7 +56,7 @@ theorem spectrum_countable_is_proven (M : CompactManifold) :
 /-
 ## What Changed in the Codebase
 
-**File**: `core/Lean/GIFT/Spectral/SpectralTheory.lean`
+**File**: `core/GIFT/Spectral/SpectralTheory.lean`
 
 **Added field to ManifoldSpectralData** (line ~251):
 ```lean

Lean/GIFT/Test/AristotleZeroEigenvalueTest.lean → GIFTTest/AristotleZeroEigenvalueTest.lean

@@ -63,7 +63,7 @@ theorem zero_eigenvalue_is_proven (M : CompactManifold) :
 /-
 ## What Changed in the Codebase
 
-**File**: `core/Lean/GIFT/Spectral/SpectralTheory.lean`
+**File**: `core/GIFT/Spectral/SpectralTheory.lean`
 
 **Converted axiom to theorem** (line ~279):
 ```lean

README.md

@@ -8,77 +8,42 @@ Formally verified mathematical relations from the GIFT framework. 460+ certified
 ## Structure
 
 ```
-Lean/GIFT/
-├── Core.lean                # Constants (dim_E8, b2, b3, H*, ...)
-├── Certificate/             # Modular certificate system
-│   ├── Core.lean            # Master: Foundations ∧ Predictions ∧ Spectral
-│   ├── Foundations.lean     # E₈, G₂, octonions, K₇, Joyce, NK cert, orthonormality, gauge (34 conjuncts)
-│   ├── Predictions.lean     # 33+ relations, ~50 observables (56 conjuncts)
-│   └── Spectral.lean        # Mass gap, TCS, computed spectrum, Weyl law (37 conjuncts)
-├── Certificate.lean         # Backward-compat wrapper (legacy aliases)
-│
-├── Foundations/              # Mathematical foundations (23 files)
-│   ├── RootSystems.lean     # E₈ roots in ℝ⁸ (240 vectors)
-│   ├── E8Lattice.lean       # E₈ lattice, Weyl reflection
-│   ├── G2CrossProduct.lean  # 7D cross product, Fano plane
-│   ├── OctonionBridge.lean  # R8-R7 connection via octonions
-│   ├── AmbroseSinger.lean   # Holonomy diagnostics (so(7)=g₂⊕g₂⊥)
-│   ├── ExplicitG2Metric.lean # 169-param Chebyshev-Cholesky
-│   ├── NewtonKantorovich.lean # NK cert: h=β·η·ω < 0.5, decomposed
-│   ├── K3HarmonicCorrection.lean # ×2995 torsion, T₀-T₅ monotone
-│   ├── Analysis/K7Orthonormality.lean # L2 Gram matrices, Gram-Schmidt
-│   ├── NumericalBounds.lean # Taylor series bounds (axiom-free)
-│   ├── GoldenRatioPowers.lean # φ power bounds
-│   ├── PoincareDuality.lean # H*=1+2*dim_K7², holonomy chain
-│   ├── ConformalRigidity.lean # G₂ rep theory, metric uniqueness
-│   ├── SpectralScaling.lean # Neumann eigenvalue hierarchy
-│   ├── TCSConstruction.lean, TCSPiecewiseMetric.lean, G2Holonomy.lean, ...
-│   └── Analysis/            # G₂ forms, Hodge theory, Sobolev
-│       └── G2Forms/         # d, ⋆, TorsionFree, Bridge
-│
-├── Geometry/                # Axiom-free DG infrastructure
-│   ├── Exterior.lean        # Λ*(ℝ⁷) exterior algebra
-│   ├── DifferentialFormsR7.lean # DiffForm, d, d²=0
-│   ├── HodgeStarCompute.lean # Explicit Hodge star (Levi-Civita)
-│   └── HodgeStarR7.lean     # ⋆, ψ=⋆φ PROVEN, TorsionFree
-│
-├── Spectral/                # Spectral gap theory (17 files)
+GIFT/                           # Lean 4 formalization (root library)
+├── Core.lean                   # Constants (dim_E8, b2, b3, H*, ...)
+├── Certificate/                # Modular certificate system
+│   ├── Core.lean               # Master: Foundations ∧ Predictions ∧ Spectral
+│   ├── Foundations.lean        # E₈, G₂, octonions, K₇, Joyce, NK cert (34 conjuncts)
+│   ├── Predictions.lean        # 33+ relations, ~50 observables (56 conjuncts)
+│   └── Spectral.lean           # Mass gap, TCS, computed spectrum, Weyl law (37 conjuncts)
+├── Foundations/                 # Mathematical foundations (23 files)
+│   ├── RootSystems.lean        # E₈ roots in ℝ⁸ (240 vectors)
+│   ├── E8Lattice.lean          # E₈ lattice, Weyl reflection
+│   ├── G2CrossProduct.lean     # 7D cross product, Fano plane
+│   ├── ExplicitG2Metric.lean   # 169-param Chebyshev-Cholesky
+│   ├── NewtonKantorovich.lean  # NK cert: h < 0.5, decomposed
+│   ├── NumericalBounds.lean    # Taylor series bounds (axiom-free)
+│   └── Analysis/               # G₂ forms, Hodge theory, Sobolev
+├── Geometry/                   # Axiom-free DG infrastructure
+│   ├── HodgeStarR7.lean        # ⋆, ψ=⋆φ PROVEN, TorsionFree
+│   └── HodgeStarCompute.lean   # Explicit Hodge star (Levi-Civita)
+├── Spectral/                   # Spectral gap theory (17 files)
 │   ├── PhysicalSpectralGap.lean # ev₁ = 13/99 (zero axioms)
-│   ├── ComputedSpectrum.lean # Q22 sig, SD/ASD gap, B-test, couplings
-│   ├── ComputedYukawa.lean  # Yukawa mass ratios (tau:mu:e)
-│   ├── ComputedWeylLaw.lean # 7D Weyl law: α=3.46, 22K+ KK states
-│   ├── SpectralDemocracy.lean # SD spread <2%, coupling ratio <1.02
-│   ├── SelectionPrinciple.lean # κ = π²/14, building blocks
-│   ├── TCSBounds.lean       # Model Theorem: ev₁ ~ 1/L²
-│   ├── NeckGeometry.lean    # TCS structure, H1-H6 hypotheses
-│   ├── CheegerInequality.lean # Cheeger-Buser bounds
-│   ├── UniversalLaw.lean    # λ₁ × H* = dim(G₂)
-│   ├── MassGapRatio.lean    # 14/99 bare algebraic
-│   ├── YangMills.lean       # Gauge theory connection
-│   └── LiteratureAxioms.lean, G2Manifold.lean, RefinedSpectralBounds.lean, SpectralTheory.lean
-│
-├── MollifiedSum/            # Mollified Dirichlet polynomial
-│   ├── Mollifier.lean       # Cosine-squared kernel w(x)
-│   ├── Sum.lean             # S_w(T) as Finset.sum over primes
-│   └── Adaptive.lean        # Adaptive cutoff θ(T) = θ₀ + θ₁/log T
-│
-├── Relations/               # Physical predictions (22 files)
-│   ├── GaugeSector.lean, LeptonSector.lean, NeutrinoSector.lean, QuarkSector.lean
-│   ├── Cosmology.lean, MassFactorization.lean, YukawaDuality.lean
-│   ├── ExceptionalGroups.lean, ExceptionalChain.lean, SO16Relations.lean
-│   ├── CompactificationCorrection.lean  # δ_CP = 197×62/69 ≈ 177.01°
-│   └── Structural.lean, BaseDecomposition.lean, IrrationalSector.lean, ...
-│
-├── Observables/             # PMNS, CKM, quark masses, cosmology
-├── Algebraic/               # Octonions, Betti numbers, G₂, SO(16)
-├── Hierarchy/               # Dimensional gap, absolute masses, E₆ cascade, TCS gauge breaking, gauge bundle, associative volumes
-│
-├── Joyce.lean               # Joyce existence theorem
-├── Sobolev.lean             # Sobolev embedding
-├── DifferentialForms.lean   # Differential forms
-└── ImplicitFunction.lean    # Implicit function theorem
-
-gift_core/                   # Python package (giftpy)
+│   ├── ComputedSpectrum.lean   # Q22 sig, SD/ASD gap, B-test
+│   └── CheegerInequality.lean  # Cheeger-Buser bounds
+├── Relations/                  # Physical predictions (22 files)
+├── Observables/                # PMNS, CKM, quark masses, cosmology
+├── Hierarchy/                  # Dimensional gap, absolute masses
+└── MollifiedSum/               # Mollified Dirichlet polynomial
+
+GIFTTest/                       # Lean test files
+
+blueprint/                      # Leanblueprint dependency graph
+
+contrib/                        # Non-Lean assets
+├── python/                     # Python package (giftpy on PyPI)
+│   └── gift_core/              # Certified constants export
+├── homepage/                   # GitHub Pages / Jekyll site
+└── docs/                       # Extended documentation
 ```
 
 ## Quick Start
@@ -98,7 +63,7 @@ print(TAU)            # Fraction(3472, 891)
 ## Building Proofs
 
 ```bash
-cd Lean && lake build
+lake build
 ```
 
 ## Documentation
@@ -109,6 +74,6 @@ For extended observables, publications, and detailed analysis:
 
 ---
 
-[Changelog](CHANGELOG.md) | [MIT License](LICENSE)
+[Changelog](contrib/CHANGELOG.md) | [MIT License](LICENSE)
 
-*GIFT Core v3.3.47*
+*GIFT Core v3.4.0*