diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 9005e95e..b0834887 100644 --- a/.github/workflows/blueprint.yml +++ b/.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' diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml index 748787e5..a03bcce3 100644 --- a/.github/workflows/publish.yml +++ b/.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/ diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index b8f63d7e..4f7b68f5 100644 --- a/.github/workflows/verify.yml +++ b/.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) diff --git a/.gitignore b/.gitignore index a99568c5..3be065a6 100644 --- a/.gitignore +++ b/.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 diff --git a/Lean/GIFT.lean b/GIFT.lean similarity index 98% rename from Lean/GIFT.lean rename to GIFT.lean index 712d6170..06eb2eea 100644 --- a/Lean/GIFT.lean +++ b/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 diff --git a/Lean/GIFT/Algebraic.lean b/GIFT/Algebraic.lean similarity index 100% rename from Lean/GIFT/Algebraic.lean rename to GIFT/Algebraic.lean diff --git a/Lean/GIFT/Algebraic/BettiNumbers.lean b/GIFT/Algebraic/BettiNumbers.lean similarity index 100% rename from Lean/GIFT/Algebraic/BettiNumbers.lean rename to GIFT/Algebraic/BettiNumbers.lean diff --git a/Lean/GIFT/Algebraic/CayleyDickson.lean b/GIFT/Algebraic/CayleyDickson.lean similarity index 100% rename from Lean/GIFT/Algebraic/CayleyDickson.lean rename to GIFT/Algebraic/CayleyDickson.lean diff --git a/Lean/GIFT/Algebraic/G2.lean b/GIFT/Algebraic/G2.lean similarity index 100% rename from Lean/GIFT/Algebraic/G2.lean rename to GIFT/Algebraic/G2.lean diff --git a/Lean/GIFT/Algebraic/GIFTConstants.lean b/GIFT/Algebraic/GIFTConstants.lean similarity index 100% rename from Lean/GIFT/Algebraic/GIFTConstants.lean rename to GIFT/Algebraic/GIFTConstants.lean diff --git a/Lean/GIFT/Algebraic/GeometricSaturation.lean b/GIFT/Algebraic/GeometricSaturation.lean similarity index 100% rename from Lean/GIFT/Algebraic/GeometricSaturation.lean rename to GIFT/Algebraic/GeometricSaturation.lean diff --git a/Lean/GIFT/Algebraic/Octonions.lean b/GIFT/Algebraic/Octonions.lean similarity index 100% rename from Lean/GIFT/Algebraic/Octonions.lean rename to GIFT/Algebraic/Octonions.lean diff --git a/Lean/GIFT/Algebraic/Quaternions.lean b/GIFT/Algebraic/Quaternions.lean similarity index 100% rename from Lean/GIFT/Algebraic/Quaternions.lean rename to GIFT/Algebraic/Quaternions.lean diff --git a/Lean/GIFT/Algebraic/SO16Decomposition.lean b/GIFT/Algebraic/SO16Decomposition.lean similarity index 100% rename from Lean/GIFT/Algebraic/SO16Decomposition.lean rename to GIFT/Algebraic/SO16Decomposition.lean diff --git a/Lean/GIFT/Certificate.lean b/GIFT/Certificate.lean similarity index 100% rename from Lean/GIFT/Certificate.lean rename to GIFT/Certificate.lean diff --git a/Lean/GIFT/Certificate/Core.lean b/GIFT/Certificate/Core.lean similarity index 100% rename from Lean/GIFT/Certificate/Core.lean rename to GIFT/Certificate/Core.lean diff --git a/Lean/GIFT/Certificate/Foundations.lean b/GIFT/Certificate/Foundations.lean similarity index 100% rename from Lean/GIFT/Certificate/Foundations.lean rename to GIFT/Certificate/Foundations.lean diff --git a/Lean/GIFT/Certificate/Predictions.lean b/GIFT/Certificate/Predictions.lean similarity index 100% rename from Lean/GIFT/Certificate/Predictions.lean rename to GIFT/Certificate/Predictions.lean diff --git a/Lean/GIFT/Certificate/Spectral.lean b/GIFT/Certificate/Spectral.lean similarity index 100% rename from Lean/GIFT/Certificate/Spectral.lean rename to GIFT/Certificate/Spectral.lean diff --git a/Lean/GIFT/Core.lean b/GIFT/Core.lean similarity index 100% rename from Lean/GIFT/Core.lean rename to GIFT/Core.lean diff --git a/Lean/GIFT/DifferentialForms.lean b/GIFT/DifferentialForms.lean similarity index 100% rename from Lean/GIFT/DifferentialForms.lean rename to GIFT/DifferentialForms.lean diff --git a/Lean/GIFT/Foundations.lean b/GIFT/Foundations.lean similarity index 100% rename from Lean/GIFT/Foundations.lean rename to GIFT/Foundations.lean diff --git a/Lean/GIFT/Foundations/AmbroseSinger.lean b/GIFT/Foundations/AmbroseSinger.lean similarity index 100% rename from Lean/GIFT/Foundations/AmbroseSinger.lean rename to GIFT/Foundations/AmbroseSinger.lean diff --git a/Lean/GIFT/Foundations/Analysis.lean b/GIFT/Foundations/Analysis.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis.lean rename to GIFT/Foundations/Analysis.lean diff --git a/Lean/GIFT/Foundations/Analysis/AnalyticalFoundations.lean b/GIFT/Foundations/Analysis/AnalyticalFoundations.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/AnalyticalFoundations.lean rename to GIFT/Foundations/Analysis/AnalyticalFoundations.lean diff --git a/Lean/GIFT/Foundations/Analysis/E8Lattice.lean b/GIFT/Foundations/Analysis/E8Lattice.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/E8Lattice.lean rename to GIFT/Foundations/Analysis/E8Lattice.lean diff --git a/Lean/GIFT/Foundations/Analysis/Elliptic/Basic.lean b/GIFT/Foundations/Analysis/Elliptic/Basic.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/Elliptic/Basic.lean rename to GIFT/Foundations/Analysis/Elliptic/Basic.lean diff --git a/Lean/GIFT/Foundations/Analysis/ExteriorAlgebra.lean b/GIFT/Foundations/Analysis/ExteriorAlgebra.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/ExteriorAlgebra.lean rename to GIFT/Foundations/Analysis/ExteriorAlgebra.lean diff --git a/Lean/GIFT/Foundations/Analysis/G2Forms/All.lean b/GIFT/Foundations/Analysis/G2Forms/All.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/G2Forms/All.lean rename to GIFT/Foundations/Analysis/G2Forms/All.lean diff --git a/Lean/GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean b/GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean rename to GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean diff --git a/Lean/GIFT/Foundations/Analysis/G2Forms/G2FormsBridge.lean b/GIFT/Foundations/Analysis/G2Forms/G2FormsBridge.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/G2Forms/G2FormsBridge.lean rename to GIFT/Foundations/Analysis/G2Forms/G2FormsBridge.lean diff --git a/Lean/GIFT/Foundations/Analysis/G2Forms/G2Structure.lean b/GIFT/Foundations/Analysis/G2Forms/G2Structure.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/G2Forms/G2Structure.lean rename to GIFT/Foundations/Analysis/G2Forms/G2Structure.lean diff --git a/Lean/GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean b/GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean rename to GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean diff --git a/Lean/GIFT/Foundations/Analysis/G2TensorForm.lean b/GIFT/Foundations/Analysis/G2TensorForm.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/G2TensorForm.lean rename to GIFT/Foundations/Analysis/G2TensorForm.lean diff --git a/Lean/GIFT/Foundations/Analysis/HarmonicForms.lean b/GIFT/Foundations/Analysis/HarmonicForms.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/HarmonicForms.lean rename to GIFT/Foundations/Analysis/HarmonicForms.lean diff --git a/Lean/GIFT/Foundations/Analysis/HodgeTheory.lean b/GIFT/Foundations/Analysis/HodgeTheory.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/HodgeTheory.lean rename to GIFT/Foundations/Analysis/HodgeTheory.lean diff --git a/Lean/GIFT/Foundations/Analysis/IFT/Basic.lean b/GIFT/Foundations/Analysis/IFT/Basic.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/IFT/Basic.lean rename to GIFT/Foundations/Analysis/IFT/Basic.lean diff --git a/Lean/GIFT/Foundations/Analysis/InnerProductSpace.lean b/GIFT/Foundations/Analysis/InnerProductSpace.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/InnerProductSpace.lean rename to GIFT/Foundations/Analysis/InnerProductSpace.lean diff --git a/Lean/GIFT/Foundations/Analysis/JoyceAnalytic.lean b/GIFT/Foundations/Analysis/JoyceAnalytic.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/JoyceAnalytic.lean rename to GIFT/Foundations/Analysis/JoyceAnalytic.lean diff --git a/Lean/GIFT/Foundations/Analysis/K7Orthonormality.lean b/GIFT/Foundations/Analysis/K7Orthonormality.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/K7Orthonormality.lean rename to GIFT/Foundations/Analysis/K7Orthonormality.lean diff --git a/Lean/GIFT/Foundations/Analysis/Sobolev/Basic.lean b/GIFT/Foundations/Analysis/Sobolev/Basic.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/Sobolev/Basic.lean rename to GIFT/Foundations/Analysis/Sobolev/Basic.lean diff --git a/Lean/GIFT/Foundations/Analysis/WedgeProduct.lean b/GIFT/Foundations/Analysis/WedgeProduct.lean similarity index 100% rename from Lean/GIFT/Foundations/Analysis/WedgeProduct.lean rename to GIFT/Foundations/Analysis/WedgeProduct.lean diff --git a/Lean/GIFT/Foundations/AnalyticalMetric.lean b/GIFT/Foundations/AnalyticalMetric.lean similarity index 100% rename from Lean/GIFT/Foundations/AnalyticalMetric.lean rename to GIFT/Foundations/AnalyticalMetric.lean diff --git a/Lean/GIFT/Foundations/ConformalRigidity.lean b/GIFT/Foundations/ConformalRigidity.lean similarity index 100% rename from Lean/GIFT/Foundations/ConformalRigidity.lean rename to GIFT/Foundations/ConformalRigidity.lean diff --git a/Lean/GIFT/Foundations/E8Lattice.lean b/GIFT/Foundations/E8Lattice.lean similarity index 100% rename from Lean/GIFT/Foundations/E8Lattice.lean rename to GIFT/Foundations/E8Lattice.lean diff --git a/Lean/GIFT/Foundations/E8Mathlib.lean b/GIFT/Foundations/E8Mathlib.lean similarity index 100% rename from Lean/GIFT/Foundations/E8Mathlib.lean rename to GIFT/Foundations/E8Mathlib.lean diff --git a/Lean/GIFT/Foundations/ExplicitG2Metric.lean b/GIFT/Foundations/ExplicitG2Metric.lean similarity index 100% rename from Lean/GIFT/Foundations/ExplicitG2Metric.lean rename to GIFT/Foundations/ExplicitG2Metric.lean diff --git a/Lean/GIFT/Foundations/G2CrossProduct.lean b/GIFT/Foundations/G2CrossProduct.lean similarity index 100% rename from Lean/GIFT/Foundations/G2CrossProduct.lean rename to GIFT/Foundations/G2CrossProduct.lean diff --git a/Lean/GIFT/Foundations/G2Holonomy.lean b/GIFT/Foundations/G2Holonomy.lean similarity index 100% rename from Lean/GIFT/Foundations/G2Holonomy.lean rename to GIFT/Foundations/G2Holonomy.lean diff --git a/Lean/GIFT/Foundations/GoldenRatio.lean b/GIFT/Foundations/GoldenRatio.lean similarity index 100% rename from Lean/GIFT/Foundations/GoldenRatio.lean rename to GIFT/Foundations/GoldenRatio.lean diff --git a/Lean/GIFT/Foundations/GoldenRatioPowers.lean b/GIFT/Foundations/GoldenRatioPowers.lean similarity index 100% rename from Lean/GIFT/Foundations/GoldenRatioPowers.lean rename to GIFT/Foundations/GoldenRatioPowers.lean diff --git a/Lean/GIFT/Foundations/GraphTheory.lean b/GIFT/Foundations/GraphTheory.lean similarity index 100% rename from Lean/GIFT/Foundations/GraphTheory.lean rename to GIFT/Foundations/GraphTheory.lean diff --git a/Lean/GIFT/Foundations/K3HarmonicCorrection.lean b/GIFT/Foundations/K3HarmonicCorrection.lean similarity index 100% rename from Lean/GIFT/Foundations/K3HarmonicCorrection.lean rename to GIFT/Foundations/K3HarmonicCorrection.lean diff --git a/Lean/GIFT/Foundations/MetricEigenvalues.lean b/GIFT/Foundations/MetricEigenvalues.lean similarity index 100% rename from Lean/GIFT/Foundations/MetricEigenvalues.lean rename to GIFT/Foundations/MetricEigenvalues.lean diff --git a/Lean/GIFT/Foundations/NewtonKantorovich.lean b/GIFT/Foundations/NewtonKantorovich.lean similarity index 100% rename from Lean/GIFT/Foundations/NewtonKantorovich.lean rename to GIFT/Foundations/NewtonKantorovich.lean diff --git a/Lean/GIFT/Foundations/NumericalBounds.lean b/GIFT/Foundations/NumericalBounds.lean similarity index 100% rename from Lean/GIFT/Foundations/NumericalBounds.lean rename to GIFT/Foundations/NumericalBounds.lean diff --git a/Lean/GIFT/Foundations/OctonionBridge.lean b/GIFT/Foundations/OctonionBridge.lean similarity index 100% rename from Lean/GIFT/Foundations/OctonionBridge.lean rename to GIFT/Foundations/OctonionBridge.lean diff --git a/Lean/GIFT/Foundations/PiBounds.lean b/GIFT/Foundations/PiBounds.lean similarity index 100% rename from Lean/GIFT/Foundations/PiBounds.lean rename to GIFT/Foundations/PiBounds.lean diff --git a/Lean/GIFT/Foundations/PoincareDuality.lean b/GIFT/Foundations/PoincareDuality.lean similarity index 100% rename from Lean/GIFT/Foundations/PoincareDuality.lean rename to GIFT/Foundations/PoincareDuality.lean diff --git a/Lean/GIFT/Foundations/RationalConstants.lean b/GIFT/Foundations/RationalConstants.lean similarity index 100% rename from Lean/GIFT/Foundations/RationalConstants.lean rename to GIFT/Foundations/RationalConstants.lean diff --git a/Lean/GIFT/Foundations/RootSystems.lean b/GIFT/Foundations/RootSystems.lean similarity index 100% rename from Lean/GIFT/Foundations/RootSystems.lean rename to GIFT/Foundations/RootSystems.lean diff --git a/Lean/GIFT/Foundations/SpectralScaling.lean b/GIFT/Foundations/SpectralScaling.lean similarity index 100% rename from Lean/GIFT/Foundations/SpectralScaling.lean rename to GIFT/Foundations/SpectralScaling.lean diff --git a/Lean/GIFT/Foundations/TCSConstruction.lean b/GIFT/Foundations/TCSConstruction.lean similarity index 100% rename from Lean/GIFT/Foundations/TCSConstruction.lean rename to GIFT/Foundations/TCSConstruction.lean diff --git a/Lean/GIFT/Foundations/TCSPiecewiseMetric.lean b/GIFT/Foundations/TCSPiecewiseMetric.lean similarity index 100% rename from Lean/GIFT/Foundations/TCSPiecewiseMetric.lean rename to GIFT/Foundations/TCSPiecewiseMetric.lean diff --git a/Lean/GIFT/Geometry.lean b/GIFT/Geometry.lean similarity index 100% rename from Lean/GIFT/Geometry.lean rename to GIFT/Geometry.lean diff --git a/Lean/GIFT/Geometry/DifferentialFormsR7.lean b/GIFT/Geometry/DifferentialFormsR7.lean similarity index 100% rename from Lean/GIFT/Geometry/DifferentialFormsR7.lean rename to GIFT/Geometry/DifferentialFormsR7.lean diff --git a/Lean/GIFT/Geometry/Exterior.lean b/GIFT/Geometry/Exterior.lean similarity index 100% rename from Lean/GIFT/Geometry/Exterior.lean rename to GIFT/Geometry/Exterior.lean diff --git a/Lean/GIFT/Geometry/HodgeStarCompute.lean b/GIFT/Geometry/HodgeStarCompute.lean similarity index 100% rename from Lean/GIFT/Geometry/HodgeStarCompute.lean rename to GIFT/Geometry/HodgeStarCompute.lean diff --git a/Lean/GIFT/Geometry/HodgeStarR7.lean b/GIFT/Geometry/HodgeStarR7.lean similarity index 100% rename from Lean/GIFT/Geometry/HodgeStarR7.lean rename to GIFT/Geometry/HodgeStarR7.lean diff --git a/Lean/GIFT/Hierarchy.lean b/GIFT/Hierarchy.lean similarity index 100% rename from Lean/GIFT/Hierarchy.lean rename to GIFT/Hierarchy.lean diff --git a/Lean/GIFT/Hierarchy/AbsoluteMasses.lean b/GIFT/Hierarchy/AbsoluteMasses.lean similarity index 100% rename from Lean/GIFT/Hierarchy/AbsoluteMasses.lean rename to GIFT/Hierarchy/AbsoluteMasses.lean diff --git a/Lean/GIFT/Hierarchy/AssociativeVolumes.lean b/GIFT/Hierarchy/AssociativeVolumes.lean similarity index 100% rename from Lean/GIFT/Hierarchy/AssociativeVolumes.lean rename to GIFT/Hierarchy/AssociativeVolumes.lean diff --git a/Lean/GIFT/Hierarchy/DimensionalGap.lean b/GIFT/Hierarchy/DimensionalGap.lean similarity index 100% rename from Lean/GIFT/Hierarchy/DimensionalGap.lean rename to GIFT/Hierarchy/DimensionalGap.lean diff --git a/Lean/GIFT/Hierarchy/E6Cascade.lean b/GIFT/Hierarchy/E6Cascade.lean similarity index 100% rename from Lean/GIFT/Hierarchy/E6Cascade.lean rename to GIFT/Hierarchy/E6Cascade.lean diff --git a/Lean/GIFT/Hierarchy/GaugeBundleData.lean b/GIFT/Hierarchy/GaugeBundleData.lean similarity index 100% rename from Lean/GIFT/Hierarchy/GaugeBundleData.lean rename to GIFT/Hierarchy/GaugeBundleData.lean diff --git a/Lean/GIFT/Hierarchy/TCSGaugeBreaking.lean b/GIFT/Hierarchy/TCSGaugeBreaking.lean similarity index 100% rename from Lean/GIFT/Hierarchy/TCSGaugeBreaking.lean rename to GIFT/Hierarchy/TCSGaugeBreaking.lean diff --git a/Lean/GIFT/Hierarchy/VacuumStructure.lean b/GIFT/Hierarchy/VacuumStructure.lean similarity index 100% rename from Lean/GIFT/Hierarchy/VacuumStructure.lean rename to GIFT/Hierarchy/VacuumStructure.lean diff --git a/Lean/GIFT/ImplicitFunction.lean b/GIFT/ImplicitFunction.lean similarity index 100% rename from Lean/GIFT/ImplicitFunction.lean rename to GIFT/ImplicitFunction.lean diff --git a/Lean/GIFT/IntervalArithmetic.lean b/GIFT/IntervalArithmetic.lean similarity index 100% rename from Lean/GIFT/IntervalArithmetic.lean rename to GIFT/IntervalArithmetic.lean diff --git a/Lean/GIFT/Joyce.lean b/GIFT/Joyce.lean similarity index 100% rename from Lean/GIFT/Joyce.lean rename to GIFT/Joyce.lean diff --git a/Lean/GIFT/MollifiedSum.lean b/GIFT/MollifiedSum.lean similarity index 100% rename from Lean/GIFT/MollifiedSum.lean rename to GIFT/MollifiedSum.lean diff --git a/Lean/GIFT/MollifiedSum/Adaptive.lean b/GIFT/MollifiedSum/Adaptive.lean similarity index 100% rename from Lean/GIFT/MollifiedSum/Adaptive.lean rename to GIFT/MollifiedSum/Adaptive.lean diff --git a/Lean/GIFT/MollifiedSum/Mollifier.lean b/GIFT/MollifiedSum/Mollifier.lean similarity index 100% rename from Lean/GIFT/MollifiedSum/Mollifier.lean rename to GIFT/MollifiedSum/Mollifier.lean diff --git a/Lean/GIFT/MollifiedSum/Sum.lean b/GIFT/MollifiedSum/Sum.lean similarity index 100% rename from Lean/GIFT/MollifiedSum/Sum.lean rename to GIFT/MollifiedSum/Sum.lean diff --git a/Lean/GIFT/Observables.lean b/GIFT/Observables.lean similarity index 100% rename from Lean/GIFT/Observables.lean rename to GIFT/Observables.lean diff --git a/Lean/GIFT/Observables/BosonMasses.lean b/GIFT/Observables/BosonMasses.lean similarity index 100% rename from Lean/GIFT/Observables/BosonMasses.lean rename to GIFT/Observables/BosonMasses.lean diff --git a/Lean/GIFT/Observables/CKM.lean b/GIFT/Observables/CKM.lean similarity index 100% rename from Lean/GIFT/Observables/CKM.lean rename to GIFT/Observables/CKM.lean diff --git a/Lean/GIFT/Observables/Cosmology.lean b/GIFT/Observables/Cosmology.lean similarity index 100% rename from Lean/GIFT/Observables/Cosmology.lean rename to GIFT/Observables/Cosmology.lean diff --git a/Lean/GIFT/Observables/PMNS.lean b/GIFT/Observables/PMNS.lean similarity index 100% rename from Lean/GIFT/Observables/PMNS.lean rename to GIFT/Observables/PMNS.lean diff --git a/Lean/GIFT/Observables/QuarkMasses.lean b/GIFT/Observables/QuarkMasses.lean similarity index 100% rename from Lean/GIFT/Observables/QuarkMasses.lean rename to GIFT/Observables/QuarkMasses.lean diff --git a/Lean/GIFT/Observables/WeakMixingAngle.lean b/GIFT/Observables/WeakMixingAngle.lean similarity index 100% rename from Lean/GIFT/Observables/WeakMixingAngle.lean rename to GIFT/Observables/WeakMixingAngle.lean diff --git a/Lean/GIFT/Relations.lean b/GIFT/Relations.lean similarity index 100% rename from Lean/GIFT/Relations.lean rename to GIFT/Relations.lean diff --git a/Lean/GIFT/Relations/BaseDecomposition.lean b/GIFT/Relations/BaseDecomposition.lean similarity index 100% rename from Lean/GIFT/Relations/BaseDecomposition.lean rename to GIFT/Relations/BaseDecomposition.lean diff --git a/Lean/GIFT/Relations/CompactificationCorrection.lean b/GIFT/Relations/CompactificationCorrection.lean similarity index 100% rename from Lean/GIFT/Relations/CompactificationCorrection.lean rename to GIFT/Relations/CompactificationCorrection.lean diff --git a/Lean/GIFT/Relations/Cosmology.lean b/GIFT/Relations/Cosmology.lean similarity index 100% rename from Lean/GIFT/Relations/Cosmology.lean rename to GIFT/Relations/Cosmology.lean diff --git a/Lean/GIFT/Relations/ExceptionalChain.lean b/GIFT/Relations/ExceptionalChain.lean similarity index 100% rename from Lean/GIFT/Relations/ExceptionalChain.lean rename to GIFT/Relations/ExceptionalChain.lean diff --git a/Lean/GIFT/Relations/ExceptionalGroups.lean b/GIFT/Relations/ExceptionalGroups.lean similarity index 100% rename from Lean/GIFT/Relations/ExceptionalGroups.lean rename to GIFT/Relations/ExceptionalGroups.lean diff --git a/Lean/GIFT/Relations/FanoSelectionPrinciple.lean b/GIFT/Relations/FanoSelectionPrinciple.lean similarity index 100% rename from Lean/GIFT/Relations/FanoSelectionPrinciple.lean rename to GIFT/Relations/FanoSelectionPrinciple.lean diff --git a/Lean/GIFT/Relations/G2MetricProperties.lean b/GIFT/Relations/G2MetricProperties.lean similarity index 100% rename from Lean/GIFT/Relations/G2MetricProperties.lean rename to GIFT/Relations/G2MetricProperties.lean diff --git a/Lean/GIFT/Relations/GaugeSector.lean b/GIFT/Relations/GaugeSector.lean similarity index 100% rename from Lean/GIFT/Relations/GaugeSector.lean rename to GIFT/Relations/GaugeSector.lean diff --git a/Lean/GIFT/Relations/GoldenRatio.lean b/GIFT/Relations/GoldenRatio.lean similarity index 100% rename from Lean/GIFT/Relations/GoldenRatio.lean rename to GIFT/Relations/GoldenRatio.lean diff --git a/Lean/GIFT/Relations/IrrationalSector.lean b/GIFT/Relations/IrrationalSector.lean similarity index 100% rename from Lean/GIFT/Relations/IrrationalSector.lean rename to GIFT/Relations/IrrationalSector.lean diff --git a/Lean/GIFT/Relations/LandauerDarkEnergy.lean b/GIFT/Relations/LandauerDarkEnergy.lean similarity index 100% rename from Lean/GIFT/Relations/LandauerDarkEnergy.lean rename to GIFT/Relations/LandauerDarkEnergy.lean diff --git a/Lean/GIFT/Relations/LeptonSector.lean b/GIFT/Relations/LeptonSector.lean similarity index 100% rename from Lean/GIFT/Relations/LeptonSector.lean rename to GIFT/Relations/LeptonSector.lean diff --git a/Lean/GIFT/Relations/MassFactorization.lean b/GIFT/Relations/MassFactorization.lean similarity index 100% rename from Lean/GIFT/Relations/MassFactorization.lean rename to GIFT/Relations/MassFactorization.lean diff --git a/Lean/GIFT/Relations/NeutrinoSector.lean b/GIFT/Relations/NeutrinoSector.lean similarity index 100% rename from Lean/GIFT/Relations/NeutrinoSector.lean rename to GIFT/Relations/NeutrinoSector.lean diff --git a/Lean/GIFT/Relations/OverDetermination.lean b/GIFT/Relations/OverDetermination.lean similarity index 100% rename from Lean/GIFT/Relations/OverDetermination.lean rename to GIFT/Relations/OverDetermination.lean diff --git a/Lean/GIFT/Relations/QuarkSector.lean b/GIFT/Relations/QuarkSector.lean similarity index 100% rename from Lean/GIFT/Relations/QuarkSector.lean rename to GIFT/Relations/QuarkSector.lean diff --git a/Lean/GIFT/Relations/SO16Relations.lean b/GIFT/Relations/SO16Relations.lean similarity index 100% rename from Lean/GIFT/Relations/SO16Relations.lean rename to GIFT/Relations/SO16Relations.lean diff --git a/Lean/GIFT/Relations/SectorClassification.lean b/GIFT/Relations/SectorClassification.lean similarity index 100% rename from Lean/GIFT/Relations/SectorClassification.lean rename to GIFT/Relations/SectorClassification.lean diff --git a/Lean/GIFT/Relations/Structural.lean b/GIFT/Relations/Structural.lean similarity index 100% rename from Lean/GIFT/Relations/Structural.lean rename to GIFT/Relations/Structural.lean diff --git a/Lean/GIFT/Relations/TauBounds.lean b/GIFT/Relations/TauBounds.lean similarity index 100% rename from Lean/GIFT/Relations/TauBounds.lean rename to GIFT/Relations/TauBounds.lean diff --git a/Lean/GIFT/Relations/V33Additions.lean b/GIFT/Relations/V33Additions.lean similarity index 100% rename from Lean/GIFT/Relations/V33Additions.lean rename to GIFT/Relations/V33Additions.lean diff --git a/Lean/GIFT/Relations/YukawaDuality.lean b/GIFT/Relations/YukawaDuality.lean similarity index 100% rename from Lean/GIFT/Relations/YukawaDuality.lean rename to GIFT/Relations/YukawaDuality.lean diff --git a/Lean/GIFT/Sobolev.lean b/GIFT/Sobolev.lean similarity index 100% rename from Lean/GIFT/Sobolev.lean rename to GIFT/Sobolev.lean diff --git a/Lean/GIFT/Spectral.lean b/GIFT/Spectral.lean similarity index 100% rename from Lean/GIFT/Spectral.lean rename to GIFT/Spectral.lean diff --git a/Lean/GIFT/Spectral/CheegerInequality.lean b/GIFT/Spectral/CheegerInequality.lean similarity index 100% rename from Lean/GIFT/Spectral/CheegerInequality.lean rename to GIFT/Spectral/CheegerInequality.lean diff --git a/Lean/GIFT/Spectral/ComputedSpectrum.lean b/GIFT/Spectral/ComputedSpectrum.lean similarity index 100% rename from Lean/GIFT/Spectral/ComputedSpectrum.lean rename to GIFT/Spectral/ComputedSpectrum.lean diff --git a/Lean/GIFT/Spectral/ComputedWeylLaw.lean b/GIFT/Spectral/ComputedWeylLaw.lean similarity index 100% rename from Lean/GIFT/Spectral/ComputedWeylLaw.lean rename to GIFT/Spectral/ComputedWeylLaw.lean diff --git a/Lean/GIFT/Spectral/ComputedYukawa.lean b/GIFT/Spectral/ComputedYukawa.lean similarity index 100% rename from Lean/GIFT/Spectral/ComputedYukawa.lean rename to GIFT/Spectral/ComputedYukawa.lean diff --git a/Lean/GIFT/Spectral/G2Manifold.lean b/GIFT/Spectral/G2Manifold.lean similarity index 100% rename from Lean/GIFT/Spectral/G2Manifold.lean rename to GIFT/Spectral/G2Manifold.lean diff --git a/Lean/GIFT/Spectral/LiteratureAxioms.lean b/GIFT/Spectral/LiteratureAxioms.lean similarity index 100% rename from Lean/GIFT/Spectral/LiteratureAxioms.lean rename to GIFT/Spectral/LiteratureAxioms.lean diff --git a/Lean/GIFT/Spectral/MassGapRatio.lean b/GIFT/Spectral/MassGapRatio.lean similarity index 100% rename from Lean/GIFT/Spectral/MassGapRatio.lean rename to GIFT/Spectral/MassGapRatio.lean diff --git a/Lean/GIFT/Spectral/NeckGeometry.lean b/GIFT/Spectral/NeckGeometry.lean similarity index 100% rename from Lean/GIFT/Spectral/NeckGeometry.lean rename to GIFT/Spectral/NeckGeometry.lean diff --git a/Lean/GIFT/Spectral/PhysicalSpectralGap.lean b/GIFT/Spectral/PhysicalSpectralGap.lean similarity index 100% rename from Lean/GIFT/Spectral/PhysicalSpectralGap.lean rename to GIFT/Spectral/PhysicalSpectralGap.lean diff --git a/Lean/GIFT/Spectral/RefinedSpectralBounds.lean b/GIFT/Spectral/RefinedSpectralBounds.lean similarity index 100% rename from Lean/GIFT/Spectral/RefinedSpectralBounds.lean rename to GIFT/Spectral/RefinedSpectralBounds.lean diff --git a/Lean/GIFT/Spectral/SelectionPrinciple.lean b/GIFT/Spectral/SelectionPrinciple.lean similarity index 100% rename from Lean/GIFT/Spectral/SelectionPrinciple.lean rename to GIFT/Spectral/SelectionPrinciple.lean diff --git a/Lean/GIFT/Spectral/SpectralDemocracy.lean b/GIFT/Spectral/SpectralDemocracy.lean similarity index 100% rename from Lean/GIFT/Spectral/SpectralDemocracy.lean rename to GIFT/Spectral/SpectralDemocracy.lean diff --git a/Lean/GIFT/Spectral/SpectralInvariants.lean b/GIFT/Spectral/SpectralInvariants.lean similarity index 100% rename from Lean/GIFT/Spectral/SpectralInvariants.lean rename to GIFT/Spectral/SpectralInvariants.lean diff --git a/Lean/GIFT/Spectral/SpectralTheory.lean b/GIFT/Spectral/SpectralTheory.lean similarity index 100% rename from Lean/GIFT/Spectral/SpectralTheory.lean rename to GIFT/Spectral/SpectralTheory.lean diff --git a/Lean/GIFT/Spectral/TCSBounds.lean b/GIFT/Spectral/TCSBounds.lean similarity index 100% rename from Lean/GIFT/Spectral/TCSBounds.lean rename to GIFT/Spectral/TCSBounds.lean diff --git a/Lean/GIFT/Spectral/UniversalLaw.lean b/GIFT/Spectral/UniversalLaw.lean similarity index 100% rename from Lean/GIFT/Spectral/UniversalLaw.lean rename to GIFT/Spectral/UniversalLaw.lean diff --git a/Lean/GIFT/Spectral/YangMills.lean b/GIFT/Spectral/YangMills.lean similarity index 100% rename from Lean/GIFT/Spectral/YangMills.lean rename to GIFT/Spectral/YangMills.lean diff --git a/Lean/GIFT/Test/AristotleAxiomTest.lean b/GIFTTest/AristotleAxiomTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleAxiomTest.lean rename to GIFTTest/AristotleAxiomTest.lean diff --git a/Lean/GIFT/Test/AristotleBuserTest.lean b/GIFTTest/AristotleBuserTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleBuserTest.lean rename to GIFTTest/AristotleBuserTest.lean diff --git a/Lean/GIFT/Test/AristotleCheegerTest.lean b/GIFTTest/AristotleCheegerTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleCheegerTest.lean rename to GIFTTest/AristotleCheegerTest.lean diff --git a/Lean/GIFT/Test/AristotleG2SpectralConstraintTest.lean b/GIFTTest/AristotleG2SpectralConstraintTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleG2SpectralConstraintTest.lean rename to GIFTTest/AristotleG2SpectralConstraintTest.lean diff --git a/Lean/GIFT/Test/AristotleHodgeIsomorphismTest.lean b/GIFTTest/AristotleHodgeIsomorphismTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleHodgeIsomorphismTest.lean rename to GIFTTest/AristotleHodgeIsomorphismTest.lean diff --git a/Lean/GIFT/Test/AristotleRayleighRefinedTest.lean b/GIFTTest/AristotleRayleighRefinedTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleRayleighRefinedTest.lean rename to GIFTTest/AristotleRayleighRefinedTest.lean diff --git a/Lean/GIFT/Test/AristotleSpectralLowerBoundTest.lean b/GIFTTest/AristotleSpectralLowerBoundTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleSpectralLowerBoundTest.lean rename to GIFTTest/AristotleSpectralLowerBoundTest.lean diff --git a/Lean/GIFT/Test/AristotleSpectralLowerRefinedTest.lean b/GIFTTest/AristotleSpectralLowerRefinedTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleSpectralLowerRefinedTest.lean rename to GIFTTest/AristotleSpectralLowerRefinedTest.lean diff --git a/Lean/GIFT/Test/AristotleSpectralUpperBoundTest.lean b/GIFTTest/AristotleSpectralUpperBoundTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleSpectralUpperBoundTest.lean rename to GIFTTest/AristotleSpectralUpperBoundTest.lean diff --git a/Lean/GIFT/Test/AristotleSpectrumCountableTest.lean b/GIFTTest/AristotleSpectrumCountableTest.lean similarity index 98% rename from Lean/GIFT/Test/AristotleSpectrumCountableTest.lean rename to GIFTTest/AristotleSpectrumCountableTest.lean index 855e79a4..05af1e5e 100644 --- a/Lean/GIFT/Test/AristotleSpectrumCountableTest.lean +++ b/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 diff --git a/Lean/GIFT/Test/AristotleSpectrumNonnegTest.lean b/GIFTTest/AristotleSpectrumNonnegTest.lean similarity index 100% rename from Lean/GIFT/Test/AristotleSpectrumNonnegTest.lean rename to GIFTTest/AristotleSpectrumNonnegTest.lean diff --git a/Lean/GIFT/Test/AristotleZeroEigenvalueTest.lean b/GIFTTest/AristotleZeroEigenvalueTest.lean similarity index 98% rename from Lean/GIFT/Test/AristotleZeroEigenvalueTest.lean rename to GIFTTest/AristotleZeroEigenvalueTest.lean index b9b697d2..1733584b 100644 --- a/Lean/GIFT/Test/AristotleZeroEigenvalueTest.lean +++ b/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 diff --git a/Lean/lakefile.toml b/Lean/lakefile.toml deleted file mode 100644 index 1a5ece17..00000000 --- a/Lean/lakefile.toml +++ /dev/null @@ -1,29 +0,0 @@ -name = "GIFT" -version = "3.3.47" -defaultTargets = ["GIFT"] -keywords = ["mathematics", "physics", "G2", "E8", "holonomy"] - -[leanOptions] -pp.unicode.fun = true -autoImplicit = false -relaxedAutoImplicit = false -linter.unnecessarySimpa = false - -[[require]] -name = "mathlib" -git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.27.0" - -[[require]] -name = "checkdecls" -git = "https://github.com/PatrickMassot/checkdecls.git" -rev = "master" - -[[require]] -name = "«doc-gen4»" -git = "https://github.com/leanprover/doc-gen4" -rev = "v4.27.0" - -[[lean_lib]] -name = "GIFT" -globs = ["GIFT.+"] diff --git a/Lean/lean-toolchain b/Lean/lean-toolchain deleted file mode 100644 index 5249182c..00000000 --- a/Lean/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.27.0 diff --git a/MANIFEST.in b/MANIFEST.in deleted file mode 100644 index 8c4afaa4..00000000 --- a/MANIFEST.in +++ /dev/null @@ -1,3 +0,0 @@ -include LICENSE -include README.md -recursive-include Lean *.lean diff --git a/README.md b/README.md index 66b7c460..22206c42 100644 --- a/README.md +++ b/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* diff --git a/CHANGELOG.md b/contrib/CHANGELOG.md similarity index 97% rename from CHANGELOG.md rename to contrib/CHANGELOG.md index ad2fc1d6..28b3ab89 100644 --- a/CHANGELOG.md +++ b/contrib/CHANGELOG.md @@ -5,6 +5,35 @@ All notable changes to GIFT Core will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [3.4.0] - 2026-03-22 + +### Summary + +**LEAN 4 STANDARD LAYOUT.** Complete repository restructuring to comply with official Lean 4 project conventions (Lake, Reservoir, community standards). Zero Lean source code changes — only file moves and configuration. + +### Changed + +- **Lean code at root**: `Lean/GIFT.lean` → `GIFT.lean`, `Lean/GIFT/` → `GIFT/` (140 files) +- **Standard test directory**: `GIFT/Test/` → `GIFTTest/` (12 Aristotle test files) +- **Lake config**: `lakefile.toml` → `lakefile.lean` (standard format, with `lean_lib` declarations) +- **Non-Lean isolation**: Python, homepage, blueprint, docs, CLAUDE.md → `contrib/` directory + - `gift_core/` → `contrib/python/gift_core/` + - `home_page/` → `contrib/homepage/` + - `blueprint/` → `contrib/blueprint/` + - `docs/` → `contrib/docs/` +- **Reservoir compliance**: `lake-manifest.json` committed (was gitignored) +- **CI workflows**: All 3 workflows updated for new paths (verify, publish, blueprint) +- **Build command**: `lake build` from root (no more `cd Lean`) +- **Dead links fixed**: 6 stale path references updated across docs and test files + +### Root structure (post-refactor) + +``` +GIFT.lean lakefile.lean LICENSE +GIFT/ lean-toolchain README.md +GIFTTest/ lake-manifest.json contrib/ +``` + ## [3.3.47] - 2026-03-21 ### Summary diff --git a/CLAUDE.md b/contrib/CLAUDE.md similarity index 95% rename from CLAUDE.md rename to contrib/CLAUDE.md index 09e580ea..85fdc443 100644 --- a/CLAUDE.md +++ b/contrib/CLAUDE.md @@ -26,49 +26,38 @@ See **Terminology Standards** section below for complete reference. ``` gift-framework/core/ -├── Lean/ # Lean 4 formal proofs -│ ├── GIFT.lean # Main entry point -│ ├── GIFT/ -│ │ ├── Core.lean # Source of truth for constants -│ │ ├── Certificate/ # Modular certificate system -│ │ │ ├── Core.lean # Master: Foundations ∧ Predictions ∧ Spectral -│ │ │ ├── Foundations.lean # E₈, G₂, octonions, K₇, Joyce -│ │ │ ├── Predictions.lean # 33+ published relations, observables -│ │ │ └── Spectral.lean # Mass gap 14/99, TCS, selection -│ │ ├── Certificate.lean # Backward-compat wrapper (legacy aliases) -│ │ │ -│ │ ├── Algebra.lean # E₈, G₂, E₇, F₄, E₆ constants -│ │ ├── Topology.lean # Betti numbers, H*, p₂ -│ │ ├── Geometry.lean # K₇, J₃(𝕆) -│ │ │ -│ │ ├── Foundations/ # Mathematical foundations -│ │ │ ├── RootSystems.lean # E₈ roots in ℝ⁸ -│ │ │ ├── E8Lattice.lean # E₈ lattice formalization (R8) -│ │ │ ├── G2CrossProduct.lean # 7D cross product (R7) -│ │ │ ├── OctonionBridge.lean # R8-R7 connection via octonions -│ │ │ ├── AmbroseSinger.lean # Holonomy diagnostics (v3.3.24) -│ │ │ ├── Analysis/ # Hodge theory, Sobolev (research) -│ │ │ └── ... -│ │ │ -│ │ ├── Algebraic/ # Octonion-based derivation -│ │ │ ├── Octonions.lean -│ │ │ ├── G2.lean -│ │ │ └── BettiNumbers.lean -│ │ │ -│ │ ├── Relations/ # Physical predictions (15+ files) -│ │ └── Joyce.lean # Joyce existence theorem -│ └── lakefile.toml -│ -├── gift_core/ # Python package -│ ├── __init__.py # Exports (update when adding constants!) -│ ├── _version.py # Version string (3.3.47) -│ ├── constants/ # Certified constants (algebra, topology, structural, physics, cosmology) -│ ├── analysis/ # Joyce certificate, intervals +├── GIFT.lean # Main entry point (root-level, Lean 4 standard) +├── GIFT/ # Lean 4 formal proofs (140 files) +│ ├── Core.lean # Source of truth for constants +│ ├── Certificate/ # Modular certificate system +│ │ ├── Core.lean # Master: Foundations ∧ Predictions ∧ Spectral +│ │ ├── Foundations.lean # E₈, G₂, octonions, K₇, Joyce +│ │ ├── Predictions.lean # 33+ published relations, observables +│ │ └── Spectral.lean # Mass gap 14/99, TCS, selection +│ ├── Foundations/ # Mathematical foundations +│ ├── Geometry/ # Axiom-free DG infrastructure +│ ├── Spectral/ # Spectral gap theory +│ ├── Relations/ # Physical predictions (22 files) │ └── ... +├── GIFTTest/ # Lean test files (Aristotle tests) +├── lakefile.lean # Lake build config (Lean 4 standard) +├── lean-toolchain # leanprover/lean4:v4.27.0 +├── lake-manifest.json # Dependency lock file +│ +├── contrib/ # Non-Lean assets +│ ├── python/ # Python package (giftpy on PyPI) +│ │ ├── gift_core/ # Certified constants export +│ │ └── pyproject.toml +│ ├── homepage/ # GitHub Pages / Jekyll site +│ ├── blueprint/ # Leanblueprint dependency graph +│ ├── docs/ # Extended documentation +│ ├── CLAUDE.md # This file +│ └── CHANGELOG.md │ └── .github/workflows/ # CI/CD ├── verify.yml # Lean 4 verification - └── publish.yml # PyPI publish on release + ├── publish.yml # PyPI publish on release + └── blueprint.yml # Leanblueprint generation ``` --- @@ -141,10 +130,10 @@ abbrev all_relations_certified := all_13_relations_certified When adding new constants: -1. Add to appropriate file in `gift_core/constants/` (algebra, topology, structural, physics, or cosmology) -2. Import in `gift_core/__init__.py` -3. Add to `__all__` list in `gift_core/__init__.py` -4. Bump version in `gift_core/_version.py` +1. Add to appropriate file in `contrib/python/gift_core/constants/` (algebra, topology, structural, physics, or cosmology) +2. Import in `contrib/python/gift_core/__init__.py` +3. Add to `__all__` list in `contrib/python/gift_core/__init__.py` +4. Bump version in `contrib/python/gift_core/_version.py` ### 3. Version Bumping (SemVer) @@ -198,7 +187,7 @@ theorem qux : ... := by ```bash # Lean 4 -cd Lean && lake build +lake build # Quick verification of constants python -c "from gift_core import *; print(GAMMA_GIFT)" @@ -208,16 +197,16 @@ python -c "from gift_core import *; print(GAMMA_GIFT)" ## Adding New Certified Relations -1. **Lean**: Create/update file in `Lean/GIFT/Relations/` +1. **Lean**: Create/update file in `GIFT/Relations/` 2. **Lean**: Add import + abbrev to appropriate `Certificate/` sub-module: - `Certificate/Foundations.lean` — math infrastructure (E₈, G₂, K₇, Joyce) - `Certificate/Predictions.lean` — physical predictions, observables - `Certificate/Spectral.lean` — spectral gap, TCS, selection 3. **Lean**: Add conjunct to the sub-module's `def statement : Prop` -4. **Python**: Add constants to appropriate file in `gift_core/constants/` -5. **Python**: Export in `gift_core/__init__.py` +4. **Python**: Add constants to appropriate file in `contrib/python/gift_core/constants/` +5. **Python**: Export in `contrib/python/gift_core/__init__.py` 6. **Docs**: Update `README.md` -8. **Version**: Bump in `gift_core/_version.py` +8. **Version**: Bump in `contrib/python/gift_core/_version.py` --- diff --git a/docs/GIFT_STATUS.md b/contrib/docs/GIFT_STATUS.md similarity index 64% rename from docs/GIFT_STATUS.md rename to contrib/docs/GIFT_STATUS.md index 12dd1ced..a3cfdaba 100644 --- a/docs/GIFT_STATUS.md +++ b/contrib/docs/GIFT_STATUS.md @@ -1,7 +1,7 @@ # GIFT Framework Status -**Version**: 3.3.47 -**Date**: 2026-03-21 +**Version**: 3.4.0 +**Date**: 2026-03-22 **Proof Systems**: Lean 4 (v4.27.0 + Mathlib v4.27.0) --- @@ -83,44 +83,34 @@ Build: `uvx leanblueprint pdf` / `uvx leanblueprint web` ## 3. Key Files ``` -Lean/GIFT/ - Core.lean # Source of truth for constants - Certificate/ # Modular certificate system - Core.lean # Master: Foundations ∧ Predictions ∧ Spectral - Foundations.lean # E₈, G₂, octonions, K₇, Joyce - Predictions.lean # 33+ relations, observables - Spectral.lean # Mass gap, TCS, spectrum, Yukawa - Certificate.lean # Backward-compat wrapper (legacy aliases) - Foundations/ # Mathematical foundations - RootSystems.lean # E₈ roots in ℝ⁸ - E8Lattice.lean # E₈ lattice formalization - G2CrossProduct.lean # 7D cross product - OctonionBridge.lean # R8-R7 connection - ExplicitG2Metric.lean # 169-param Chebyshev-Cholesky - NewtonKantorovich.lean # NK cert: h=6.65e-8 - K3HarmonicCorrection.lean # ×2995 torsion reduction - NumericalBounds.lean # Taylor series bounds - GoldenRatioPowers.lean # φ powers - PoincareDuality.lean # H*=1+2*dim_K7^2 - ConformalRigidity.lean # G₂ rep theory, metric uniqueness - SpectralScaling.lean # Neumann eigenvalue hierarchy - TCSPiecewiseMetric.lean # Building block asymmetry - Analysis/ # G₂ forms infrastructure - Geometry/ # Axiom-free DG infrastructure - Spectral/ # Spectral gap theory, computed spectrum, Yukawa - MollifiedSum/ # Cosine-squared kernel, S_w(T) - Relations/ # Physical predictions - Observables/ # PMNS, CKM, quark masses, cosmology - Algebraic/ # Octonions, Betti numbers - Hierarchy/ # Dimensional gap, golden ratio - -gift_core/ # Python package (giftpy) - _version.py # Version 3.3.31 - constants/ # All certified constants - roots.py # E₈ root system (240 vectors) - fano.py # Fano plane, G₂ cross product - verify.py # Verification suite - relations.py # Proven relations +GIFT/ # Lean 4 formalization (root-level) + Core.lean # Source of truth for constants + Certificate/ # Modular certificate system + Core.lean # Master: Foundations ∧ Predictions ∧ Spectral + Foundations.lean # E₈, G₂, octonions, K₇, Joyce + Predictions.lean # 33+ relations, observables + Spectral.lean # Mass gap, TCS, spectrum, Yukawa + Foundations/ # Mathematical foundations + RootSystems.lean # E₈ roots in ℝ⁸ + ExplicitG2Metric.lean # 169-param Chebyshev-Cholesky + NewtonKantorovich.lean # NK cert: h=6.65e-8 + NumericalBounds.lean # Taylor series bounds + Analysis/ # G₂ forms infrastructure + Geometry/ # Axiom-free DG infrastructure + Spectral/ # Spectral gap theory, computed spectrum, Yukawa + Relations/ # Physical predictions + Observables/ # PMNS, CKM, quark masses, cosmology + Hierarchy/ # Dimensional gap, golden ratio + +GIFTTest/ # Lean test files (Aristotle tests) + +contrib/ + python/gift_core/ # Python package (giftpy on PyPI) + python/gift_core/ # Python package (giftpy on PyPI) + homepage/ # GitHub Pages / Jekyll site + docs/ # Extended documentation + +blueprint/ # Leanblueprint dependency graph (root-level, Lean convention) ``` --- @@ -129,6 +119,8 @@ gift_core/ # Python package (giftpy) | Version | Date | Highlights | |---------|------|------------| +| 3.4.0 | 2026-03-22 | Lean 4 standard layout: GIFT/ at root, lakefile.lean, contrib/, GIFTTest/ | +| 3.3.47 | 2026-03-21 | Aristotle Tier C: 13 → 11 axioms, IsEigenvalue + spectrum_nonneg eliminated | | 3.3.31 | 2026-03-08 | Tier C closure: Neumann gap, Yukawa mass ratios, exploratory cleanup | | 3.3.30 | 2026-03-08 | Spectral democracy: SD spread <2%, coupling ratio <1.02 | | 3.3.29 | 2026-03-08 | Computed spectrum: Q₂₂ (3,19), SD/ASD gap, B-test | @@ -153,4 +145,4 @@ GIFT bridges three active research programs: --- -*Updated: 2026-03-09* +*Updated: 2026-03-22* diff --git a/docs/USAGE.md b/contrib/docs/USAGE.md similarity index 99% rename from docs/USAGE.md rename to contrib/docs/USAGE.md index f8fded2c..0322e54d 100644 --- a/docs/USAGE.md +++ b/contrib/docs/USAGE.md @@ -335,7 +335,7 @@ print(cert.safety_margin) # ~20.4x ## Building Proofs Locally ```bash -cd Lean && lake build +lake build ``` ## Blueprint diff --git a/docs/index.md b/contrib/docs/index.md similarity index 79% rename from docs/index.md rename to contrib/docs/index.md index 9905124b..2c5b85d7 100644 --- a/docs/index.md +++ b/contrib/docs/index.md @@ -10,9 +10,9 @@ This directory contains documentation for the GIFT Core formal verification proj ## Quick Links - [GitHub Repository](https://github.com/gift-framework/core) -- [Blueprint (web)](../blueprint/) -- [API Documentation](../blueprint/docs/) +- [Blueprint (web)](../../blueprint/) +- [API Documentation](../../blueprint/docs/) ## Version -GIFT Core v3.3.47 +GIFT Core v3.4.0 diff --git a/home_page/404.html b/contrib/homepage/404.html similarity index 100% rename from home_page/404.html rename to contrib/homepage/404.html diff --git a/home_page/Gemfile b/contrib/homepage/Gemfile similarity index 100% rename from home_page/Gemfile rename to contrib/homepage/Gemfile diff --git a/home_page/_config.yml b/contrib/homepage/_config.yml similarity index 100% rename from home_page/_config.yml rename to contrib/homepage/_config.yml diff --git a/home_page/_layouts/default.html b/contrib/homepage/_layouts/default.html similarity index 100% rename from home_page/_layouts/default.html rename to contrib/homepage/_layouts/default.html diff --git a/home_page/gift_blueprint.html b/contrib/homepage/gift_blueprint.html similarity index 100% rename from home_page/gift_blueprint.html rename to contrib/homepage/gift_blueprint.html diff --git a/home_page/index.md b/contrib/homepage/index.md similarity index 79% rename from home_page/index.md rename to contrib/homepage/index.md index d7946395..a297b022 100644 --- a/home_page/index.md +++ b/contrib/homepage/index.md @@ -8,7 +8,7 @@ GIFT derives Standard Model parameters from E₈ × E₈ gauge theory compactifi ## Quick Links -* [**GIFT Blueprint v3.3.47**]({{ site.baseurl }}/gift_blueprint.html) - Dependency graph visualization +* [**GIFT Blueprint v3.4.0**]({{ site.baseurl }}/gift_blueprint.html) - Dependency graph visualization * [Blueprint (web)]({{ site.baseurl }}/blueprint/) - Lean blueprint with proofs * [Blueprint (pdf)]({{ site.baseurl }}/blueprint.pdf) - Downloadable PDF * [Dependency Graph]({{ site.baseurl }}/blueprint/dep_graph_document.html) - Proof dependencies @@ -26,9 +26,10 @@ GIFT derives Standard Model parameters from E₈ × E₈ gauge theory compactifi ``` gift-framework/core/ -├── Lean/ # Lean 4 formal proofs (455+ relations) -├── blueprint/ # Mathematical documentation -└── gift_core/ # Python package +├── GIFT/ # Lean 4 formal proofs (460+ relations) +├── GIFTTest/ # Lean test files +├── contrib/ # Python package, blueprint, docs +└── lakefile.lean # Lake build configuration ``` ## Getting Started @@ -39,7 +40,7 @@ git clone https://github.com/gift-framework/core.git cd core # Build Lean proofs -cd Lean && lake build +lake build # Install Python package pip install giftpy diff --git a/contrib/python/MANIFEST.in b/contrib/python/MANIFEST.in new file mode 100644 index 00000000..4dad138b --- /dev/null +++ b/contrib/python/MANIFEST.in @@ -0,0 +1,3 @@ +include ../../LICENSE +include ../../README.md +recursive-include ../../GIFT *.lean diff --git a/gift_core/__init__.py b/contrib/python/gift_core/__init__.py similarity index 99% rename from gift_core/__init__.py rename to contrib/python/gift_core/__init__.py index 4755eacc..9539c5b2 100644 --- a/gift_core/__init__.py +++ b/contrib/python/gift_core/__init__.py @@ -4,7 +4,7 @@ All values proven in Lean 4. 460+ certified relations, 11 published axioms, modular certificate structure. -v3.3.47 Features: +v3.4.0 Features: - Certificate Modularization: Foundations / Predictions / Spectral pillars - Spectral Theory: Mass gap λ₁ = 14/99, TCS bounds, Yang-Mills connection - Computed Spectrum: Q₂₂ signature (3,19), SD/ASD gap >2000× diff --git a/contrib/python/gift_core/_version.py b/contrib/python/gift_core/_version.py new file mode 100644 index 00000000..903a158a --- /dev/null +++ b/contrib/python/gift_core/_version.py @@ -0,0 +1 @@ +__version__ = "3.4.0" diff --git a/gift_core/analysis/__init__.py b/contrib/python/gift_core/analysis/__init__.py similarity index 100% rename from gift_core/analysis/__init__.py rename to contrib/python/gift_core/analysis/__init__.py diff --git a/gift_core/analysis/intervals.py b/contrib/python/gift_core/analysis/intervals.py similarity index 100% rename from gift_core/analysis/intervals.py rename to contrib/python/gift_core/analysis/intervals.py diff --git a/gift_core/analysis/joyce_certificate.py b/contrib/python/gift_core/analysis/joyce_certificate.py similarity index 100% rename from gift_core/analysis/joyce_certificate.py rename to contrib/python/gift_core/analysis/joyce_certificate.py diff --git a/gift_core/constants/__init__.py b/contrib/python/gift_core/constants/__init__.py similarity index 99% rename from gift_core/constants/__init__.py rename to contrib/python/gift_core/constants/__init__.py index b2801a72..3576bc46 100644 --- a/gift_core/constants/__init__.py +++ b/contrib/python/gift_core/constants/__init__.py @@ -1,5 +1,5 @@ """ -GIFT Constants Package (v3.3.47). +GIFT Constants Package (v3.4.0). All certified constants organized by theme: - algebra: E8, G2, F4, E6, E7, Weyl group diff --git a/gift_core/constants/algebra.py b/contrib/python/gift_core/constants/algebra.py similarity index 100% rename from gift_core/constants/algebra.py rename to contrib/python/gift_core/constants/algebra.py diff --git a/gift_core/constants/cosmology.py b/contrib/python/gift_core/constants/cosmology.py similarity index 100% rename from gift_core/constants/cosmology.py rename to contrib/python/gift_core/constants/cosmology.py diff --git a/gift_core/constants/physics.py b/contrib/python/gift_core/constants/physics.py similarity index 100% rename from gift_core/constants/physics.py rename to contrib/python/gift_core/constants/physics.py diff --git a/gift_core/constants/structural.py b/contrib/python/gift_core/constants/structural.py similarity index 100% rename from gift_core/constants/structural.py rename to contrib/python/gift_core/constants/structural.py diff --git a/gift_core/constants/topology.py b/contrib/python/gift_core/constants/topology.py similarity index 100% rename from gift_core/constants/topology.py rename to contrib/python/gift_core/constants/topology.py diff --git a/gift_core/experimental.py b/contrib/python/gift_core/experimental.py similarity index 100% rename from gift_core/experimental.py rename to contrib/python/gift_core/experimental.py diff --git a/gift_core/fano.py b/contrib/python/gift_core/fano.py similarity index 100% rename from gift_core/fano.py rename to contrib/python/gift_core/fano.py diff --git a/gift_core/monte_carlo.py b/contrib/python/gift_core/monte_carlo.py similarity index 100% rename from gift_core/monte_carlo.py rename to contrib/python/gift_core/monte_carlo.py diff --git a/gift_core/numerical_observations.py b/contrib/python/gift_core/numerical_observations.py similarity index 100% rename from gift_core/numerical_observations.py rename to contrib/python/gift_core/numerical_observations.py diff --git a/gift_core/physics/__init__.py b/contrib/python/gift_core/physics/__init__.py similarity index 100% rename from gift_core/physics/__init__.py rename to contrib/python/gift_core/physics/__init__.py diff --git a/gift_core/physics/coupling_constants.py b/contrib/python/gift_core/physics/coupling_constants.py similarity index 100% rename from gift_core/physics/coupling_constants.py rename to contrib/python/gift_core/physics/coupling_constants.py diff --git a/gift_core/physics/mass_spectrum.py b/contrib/python/gift_core/physics/mass_spectrum.py similarity index 100% rename from gift_core/physics/mass_spectrum.py rename to contrib/python/gift_core/physics/mass_spectrum.py diff --git a/gift_core/physics/yukawa_tensor.py b/contrib/python/gift_core/physics/yukawa_tensor.py similarity index 100% rename from gift_core/physics/yukawa_tensor.py rename to contrib/python/gift_core/physics/yukawa_tensor.py diff --git a/gift_core/relations.py b/contrib/python/gift_core/relations.py similarity index 100% rename from gift_core/relations.py rename to contrib/python/gift_core/relations.py diff --git a/gift_core/roots.py b/contrib/python/gift_core/roots.py similarity index 100% rename from gift_core/roots.py rename to contrib/python/gift_core/roots.py diff --git a/gift_core/scales.py b/contrib/python/gift_core/scales.py similarity index 100% rename from gift_core/scales.py rename to contrib/python/gift_core/scales.py diff --git a/gift_core/topology.py b/contrib/python/gift_core/topology.py similarity index 100% rename from gift_core/topology.py rename to contrib/python/gift_core/topology.py diff --git a/gift_core/verify.py b/contrib/python/gift_core/verify.py similarity index 100% rename from gift_core/verify.py rename to contrib/python/gift_core/verify.py diff --git a/gift_core/visualize.py b/contrib/python/gift_core/visualize.py similarity index 100% rename from gift_core/visualize.py rename to contrib/python/gift_core/visualize.py diff --git a/pyproject.toml b/contrib/python/pyproject.toml similarity index 97% rename from pyproject.toml rename to contrib/python/pyproject.toml index 62078be7..7e6dbbac 100644 --- a/pyproject.toml +++ b/contrib/python/pyproject.toml @@ -6,7 +6,7 @@ build-backend = "setuptools.build_meta" name = "giftpy" dynamic = ["version"] description = "GIFT mathematical core - Formally verified constants (Lean 4)" -readme = "README.md" +readme = "../../README.md" license = {text = "MIT"} authors = [ {name = "Brieuc de La Fourniere", email = "brieuc@bdelaf.com"} @@ -34,7 +34,7 @@ dependencies = [] Homepage = "https://github.com/gift-framework/core" Documentation = "https://github.com/gift-framework/GIFT" Repository = "https://github.com/gift-framework/core" -"Lean Proofs" = "https://github.com/gift-framework/core/tree/main/Lean" +"Lean Proofs" = "https://github.com/gift-framework/core/tree/main/GIFT" [project.optional-dependencies] dev = ["pytest>=7.0", "pytest-cov", "black", "ruff"] diff --git a/gift_core/_version.py b/gift_core/_version.py deleted file mode 100644 index a6bfe023..00000000 --- a/gift_core/_version.py +++ /dev/null @@ -1 +0,0 @@ -__version__ = "3.3.47" diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 00000000..1e097e3a --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,145 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "417747790f580618f991d0b30373a0e4d19868a2", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", + "name": "checkdecls", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "28e0856d4424863a85b18f38868c5420c55f9bae", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "8668e1ab7c987fb8ed1349f14c3b7b60bd5f27b6", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "1c5c543d2637aebf90c80aead2d401ae88db13cc", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "92a0bac89cf9f9f7cb813484506e3fb7f7350ad4", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c04225ee7c0585effbd933662b3151f01b600e40", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.85", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "GIFT", + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 00000000..40f2da9e --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,26 @@ +import Lake +open Lake DSL + +package «GIFT» + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ "v4.27.0" + +require checkdecls from git + "https://github.com/PatrickMassot/checkdecls.git" @ "master" + +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "v4.27.0" + +@[default_target] +lean_lib «GIFT» where + globs := #[.submodules `GIFT] + leanOptions := #[ + ⟨`pp.unicode.fun, true⟩, + ⟨`autoImplicit, false⟩, + ⟨`relaxedAutoImplicit, false⟩, + ⟨`linter.unnecessarySimpa, false⟩ + ] + +lean_lib «GIFTTest» where + globs := #[.submodules `GIFTTest] diff --git a/lakefile.toml b/lakefile.toml deleted file mode 100644 index c8a89457..00000000 --- a/lakefile.toml +++ /dev/null @@ -1,31 +0,0 @@ -# Root lakefile for leanblueprint compatibility -# The actual Lean project is in Lean/ - -name = "GIFT" -version = "3.3.47" -defaultTargets = ["GIFT"] - -[leanOptions] -pp.unicode.fun = true -autoImplicit = false -relaxedAutoImplicit = false - -[[require]] -name = "mathlib" -git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.27.0" - -[[require]] -name = "checkdecls" -git = "https://github.com/PatrickMassot/checkdecls.git" -rev = "master" - -[[require]] -name = "doc-gen4" -git = "https://github.com/leanprover/doc-gen4" -rev = "v4.27.0" - -[[lean_lib]] -name = "GIFT" -srcDir = "Lean" -globs = ["GIFT.+"]