Modernize Lean and clarify the scope of the formal results

.github/workflows/verify-consistency.yml

@@ -52,10 +52,5 @@ jobs:
       - name: Check blueprint sync
         run: ./scripts/check_blueprint_sync.sh
 
-      - name: Check no sorry in Lean files
-        run: |
-          if grep -rn "sorry" GIFT/ GIFTTest/ --include="*.lean" | grep -v "^.*:.*--.*sorry" | grep -v "REMOVED\|eliminated\|no.*sorry\|zero.*sorry\|all goals closed"; then
-            echo "::error::Found 'sorry' in Lean files"
-            exit 1
-          fi
-          echo "✓ Zero sorry"
+      - name: Check proof inventory
+        run: python3 scripts/proof_inventory.py --check

.github/workflows/verify.yml

@@ -2,40 +2,51 @@ name: Formal Verification
 
 on:
   push:
-    branches: [main]
-    paths: ['GIFT/**', 'GIFTTest/**', 'lakefile.lean', 'lean-toolchain']
+    branches: [main, codex/lean-modernization]
   pull_request:
     branches: [main]
   workflow_dispatch:
   workflow_call:
 
+concurrency:
+  group: lean-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   lean:
     name: Lean 4 Verification
     runs-on: ubuntu-latest
+    env:
+      LEAN_NUM_THREADS: 2
     steps:
       - uses: actions/checkout@v4
-
       - name: Install elan
         run: |
-          curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Cache .lake
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Cache dependencies
         uses: actions/cache@v4
         with:
           path: .lake
-          key: lean-${{ hashFiles('lakefile.lean') }}
-
-      - name: Build
+          key: lean-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.lean', 'lake-manifest.json') }}
+      - name: Source checks
         run: |
-          lake update
-          lake exe cache get || true
-          lake build
-
-      - name: Verify zero sorry
+          python3 scripts/test_proof_inventory.py
+          python3 scripts/proof_inventory.py --check --write docs/proof-inventory.json
+          python3 scripts/update_verification_imports.py --check
+          git diff --exit-code -- docs/proof-inventory.json
+      - name: Fetch Mathlib cache
+        run: lake exe cache get
+      - name: Build and audit proof dependencies
         run: |
-          if grep -r "sorry" GIFT/ GIFTTest/ --include="*.lean"; then
-            echo "ERROR: Found sorry!"
-            exit 1
-          fi
+          set -o pipefail
+          lake build
+          lake build Verification | tee axiom-audit.log
+          git diff --exit-code -- lake-manifest.json
+      - name: Upload verification log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: axiom-audit
+          path: axiom-audit.log
+          if-no-files-found: ignore

CONTRIBUTING.md

@@ -9,15 +9,21 @@ bound, a statement found to say less than it appears to.
 
 Org-wide rules (what helps, what does not, house style) are in the
 [organization CONTRIBUTING](https://github.com/arithmon/.github/blob/main/CONTRIBUTING.md).
-This file covers the four procedures this repository owns.
+This file covers the procedures this repository owns.
+
+Use standard mathematical names that describe the actual Lean type. Keep docstrings
+for hypotheses, conventions and proof ideas; put research histories in accompanying
+documents. Existing public names may be kept as compatibility aliases.
+
+Routine builds use the committed lockfile. Run `lake update` only during an
+intentional dependency migration and commit the updated manifest.
 
 ## Build before you open anything
 
-Continuous integration runs `lake build` and then refuses any occurrence of
-`sorry` in the Lean sources. A branch that does not build is not reviewable,
+Continuous integration runs `lake build` and audits transitive axiom dependencies and rejects proof holes. A branch that does not build is not reviewable,
 and the policy is not negotiated per pull request.
 
-1. `lake update && lake exe cache get && lake build` must succeed locally.
+1. `lake exe cache get && lake build && lake build Verification` must succeed locally.
 2. No `sorry`, and no axiom introduced to avoid one. An incomplete proof is
    better opened as an issue than merged behind a placeholder.
 3. Mathlib is the default source of standard results. Restating one locally

GIFT.lean

@@ -1,48 +1,21 @@
--- GIFT: Geometric Integration of Fundamental Topologies
--- Main entry point for Lean 4 formalization
--- Version: 3.5 (213 certificate conjuncts across 10 master certificates, 15 classified axioms (A-F taxonomy, of which 4 external data packages), 0 sorry)
-
--- ═══════════════════════════════════════════════════════════════════════════════
--- CORE & RELATIONS
--- ═══════════════════════════════════════════════════════════════════════════════
-
 import GIFT.Core
 import GIFT.Relations
 import GIFT.Relations.GaugeSector
 import GIFT.Relations.NeutrinoSector
 import GIFT.Relations.LeptonSector
 import GIFT.Relations.Cosmology
 import GIFT.Relations.CompactificationCorrection
-
--- ═══════════════════════════════════════════════════════════════════════════════
--- MATHEMATICAL FOUNDATIONS
--- ═══════════════════════════════════════════════════════════════════════════════
-
 import GIFT.Foundations
 import GIFT.Algebraic
 import GIFT.Geometry
-
--- Joyce existence theorem
 import GIFT.Sobolev
 import GIFT.DifferentialForms
 import GIFT.ImplicitFunction
 import GIFT.IntervalArithmetic
 import GIFT.Joyce
-
--- Dimensional hierarchy & golden ratio
 import GIFT.Foundations.GoldenRatioPowers
 import GIFT.Hierarchy
-
--- ═══════════════════════════════════════════════════════════════════════════════
--- OBSERVABLES & SPECTRAL THEORY
--- ═══════════════════════════════════════════════════════════════════════════════
-
 import GIFT.Observables
 import GIFT.Spectral
 import GIFT.Predictions.CP.DeltaCPNuBarConjecture
-
--- ═══════════════════════════════════════════════════════════════════════════════
--- CERTIFICATE (modular: Foundations / Predictions / Spectral)
--- ═══════════════════════════════════════════════════════════════════════════════
-
 import GIFT.Certificate.Core

GIFT/Algebraic/BettiNumbers.lean

@@ -1,64 +1,31 @@
-/-
-  GIFT Algebraic Foundations: Betti Numbers from Octonions
-  ========================================================
-
-  Betti numbers from octonion combinatorics.
-
-  THIS IS THE KEY FILE: We derive the Betti numbers b₂ and b₃
-  from the octonion structure, rather than defining them arbitrarily.
-
-  Main results:
-  - b₂ = C(|Im(𝕆)|, 2) = C(7,2) = 21
-  - b₃ = 3 × b₂ + dim(G₂) = 3 × 21 + 14 = 77
-  - H* = b₂ + b₃ + 1 = 99
-
-  These are NOT arbitrary numbers - they DERIVE from:
-  - The 7 imaginary units of 𝕆
-  - The 14-dimensional automorphism group G₂
--/
-
 import Mathlib.Data.Nat.Choose.Basic
 import Mathlib.Tactic.Ring
 import GIFT.Algebraic.Octonions
 import GIFT.Algebraic.G2
 
-namespace GIFT.Algebraic.BettiNumbers
-
-open Octonions G2
-
 /-!
-## b₂ from Octonion Structure
+Arithmetic definitions of the framework parameters b₂, b₃ and H*.
+These computations do not identify the parameters with the cohomology of a constructed manifold.
+-/
 
-b₂ = C(7,2) = 21
+namespace GIFT.Algebraic.BettiNumbers
 
-This counts pairs of imaginary units in 𝕆.
-Geometrically: 2-forms on a G₂ 7-manifold decompose into
-Ω²₇ ⊕ Ω²₁₄ with dimensions 7 + 14 = 21.
--/
+open Octonions G2
 
 /-- b₂ defined from octonion imaginary pairs -/
 def b2 : ℕ := Nat.choose imaginary_count 2
 
 /-- b₂ = 21 -/
-theorem b2_eq : b2 = 21 := by native_decide
+theorem b2_eq : b2 = 21 := by decide
 
 /-- b₂ derives from octonion structure -/
 theorem b2_from_octonions :
     b2 = Nat.choose 7 2 := rfl
 
-/-- Alternative: b₂ = Ω²₇ + Ω²₁₄ (G₂ decomposition of 2-forms) -/
+/-- Equality of the arithmetic parameter with the sum of the declared dimensions. -/
 theorem b2_from_G2_forms :
     b2 = G2.omega2_7 + G2.omega2_14 := rfl
 
-/-!
-## E₇ Fundamental Representation
-
-The 56-dimensional fundamental representation of E₇ appears
-in the derivation of b₃.
-
-fund(E₇) = 56 = 2 × b₂ + dim(G₂) = 2 × 21 + 14
--/
-
 /-- Fundamental representation dimension of E₇ -/
 def fund_E7 : ℕ := 56
 
@@ -72,18 +39,6 @@ theorem fund_E7_decomposition :
 theorem fund_E7_forms :
     fund_E7 = imaginary_count + b2 + b2 + imaginary_count := rfl
 
-/-!
-## b₃ from Octonion and G₂ Structure
-
-b₃ = 3 × b₂ + dim(G₂) = 3 × 21 + 14 = 77
-
-This formula encodes:
-- 3 copies of b₂ (from triple structure in TCS construction)
-- Plus the G₂ dimension (from holonomy)
-
-Equivalently: b₃ = b₂ + fund(E₇)
--/
-
 /-- b₃ defined from b₂ and dim(G₂) -/
 def b3 : ℕ := 3 * b2 + dim_G2
 
@@ -100,14 +55,6 @@ def N_gen : ℕ := 3
 
 theorem b3_with_Ngen : b3 = N_gen * b2 + dim_G2 := rfl
 
-/-!
-## H* = Total Hodge Number
-
-H* = b₂ + b₃ + 1 = 21 + 77 + 1 = 99
-
-The "+1" comes from the trivial cohomology H⁰.
--/
-
 /-- Total effective degrees of freedom -/
 def H_star : ℕ := b2 + b3 + 1
 
@@ -121,12 +68,6 @@ theorem H_star_formula : H_star = 4 * b2 + dim_G2 + 1 := rfl
 theorem H_star_from_octonions :
     H_star = 4 * Nat.choose imaginary_count 2 + 2 * imaginary_count + 1 := rfl
 
-/-!
-## Key Relations
-
-Verifying that everything is consistent.
--/
-
 /-- b₃ > b₂ (third Betti larger than second) -/
 theorem b3_gt_b2 : b3 > b2 := by decide
 
@@ -136,12 +77,6 @@ theorem b3_minus_b2 : b3 - b2 = fund_E7 := rfl
 /-- H* - 1 = b₂ + b₃ -/
 theorem H_star_minus_one : H_star - 1 = b2 + b3 := rfl
 
-/-!
-## Ratio Relations (for GIFT constants)
-
-These ratios are used for physical predictions in GIFTConstants.
--/
-
 /-- b₂ / imaginary_count = 3 (each imaginary appears in 3 pairs) -/
 theorem b2_per_imaginary : b2 / imaginary_count = 3 := rfl
 
@@ -150,27 +85,12 @@ theorem denominator_sin2_theta :
     b3 + dim_G2 = 91 := rfl
 
 /-- GCD(21, 91) = 7 (simplifies to 3/13) -/
-theorem sin2_theta_gcd : Nat.gcd 21 91 = 7 := by native_decide
+theorem sin2_theta_gcd : Nat.gcd 21 91 = 7 := by decide
 
 /-- dim(G₂) / b₂ = 14/21 = 2/3 (Koide ratio) -/
 theorem koide_numerator : dim_G2 = 14 := rfl
 theorem koide_denominator : b2 = 21 := b2_eq
-theorem koide_gcd : Nat.gcd 14 21 = 7 := by native_decide
-
-/-!
-## Summary: Derivation Chain
-
-ℍ → 𝕆 → G₂ → b₂, b₃ → GIFT
-
-1. 𝕆 has 7 imaginary units (from Cayley-Dickson)
-2. G₂ = Aut(𝕆) has dimension 14 = 2×7
-3. b₂ = C(7,2) = 21 (pairs of imaginary units)
-4. fund(E₇) = 56 = 2×21 + 14 (from E₇ representation theory)
-5. b₃ = b₂ + fund(E₇) = 21 + 56 = 77
-6. H* = b₂ + b₃ + 1 = 99
-
-These are DERIVED from algebraic structure, not arbitrary inputs!
--/
+theorem koide_gcd : Nat.gcd 14 21 = 7 := by decide
 
 /-- Master derivation theorem -/
 theorem betti_from_octonions :
@@ -180,6 +100,6 @@ theorem betti_from_octonions :
     b3 = b2 + fund_E7 ∧
     H_star = b2 + b3 + 1 ∧
     b2 = 21 ∧ b3 = 77 ∧ H_star = 99 :=
-  ⟨rfl, rfl, rfl, rfl, rfl, by native_decide, rfl, rfl⟩
+  ⟨rfl, rfl, rfl, rfl, rfl, by decide, rfl, rfl⟩
 
 end GIFT.Algebraic.BettiNumbers

GIFT/Algebraic/CayleyDickson.lean

@@ -126,21 +126,21 @@ This decomposes the 21 = C(7,2) pairs of octonion imaginaries.
 -/
 
 /-- C(3,2) = 3 : pairs within ℍ imaginaries -/
-theorem pairs_in_H : Nat.choose 3 2 = 3 := by native_decide
+theorem pairs_in_H : Nat.choose 3 2 = 3 := by decide
 
 /-- C(4,2) = 6 : pairs within new imaginaries -/
-theorem pairs_in_new : Nat.choose 4 2 = 6 := by native_decide
+theorem pairs_in_new : Nat.choose 4 2 = 6 := by decide
 
 /-- 3 × 4 = 12 : mixed pairs (one from ℍ, one new) -/
 theorem mixed_pairs : 3 * 4 = 12 := rfl
 
 /-- Total: 3 + 6 + 12 = 21 = b₂ -/
 theorem pairs_decomposition :
-    Nat.choose 3 2 + Nat.choose 4 2 + 3 * 4 = 21 := by native_decide
+    Nat.choose 3 2 + Nat.choose 4 2 + 3 * 4 = 21 := by decide
 
 /-- This equals C(7,2) -/
 theorem pairs_total :
-    Nat.choose 3 2 + Nat.choose 4 2 + 3 * 4 = Nat.choose 7 2 := by native_decide
+    Nat.choose 3 2 + Nat.choose 4 2 + 3 * 4 = Nat.choose 7 2 := by decide
 
 /-!
 ## Quaternion Subalgebras in 𝕆