Develop a no-sorry proof of the five-dimensional Geode value

.github/workflows/geode5-formal-proof-audit.yml

@@ -0,0 +1,116 @@
+name: Geode5 formal proof audit
+
+on:
+  push:
+    branches: [geode5-formal-proof]
+    paths:
+      - 'proofs/geode5/**'
+      - '.github/workflows/geode5-formal-proof-audit.yml'
+  pull_request:
+    branches: [main]
+    paths:
+      - 'proofs/geode5/**'
+      - '.github/workflows/geode5-formal-proof-audit.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: geode5-formal-proof-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  certificate:
+    name: Check Geode5 proof layers
+    runs-on: ubuntu-latest
+    timeout-minutes: 90
+    steps:
+      - name: Checkout proof playground
+        uses: actions/checkout@v4
+        with:
+          path: controller
+
+      - name: Checkout immutable Formal Conjectures base
+        uses: actions/checkout@v4
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: 6db9713c4c2036afdad119eda930b4d1a8da3250
+          path: target
+
+      - name: Install proof modules and certificate data
+        shell: bash
+        run: |
+          set -euo pipefail
+          dst=target/FormalConjectures/Arxiv/2508.10245/Geode5Proof
+          mkdir -p "$dst/data"
+          cp controller/proofs/geode5/Geode5CRT.lean "$dst/CRT.lean"
+          cp controller/proofs/geode5/Geode5MomentAlgebra.lean "$dst/MomentAlgebra.lean"
+          cp controller/proofs/geode5/Geode5Integral.lean "$dst/Integral.lean"
+          cp controller/proofs/geode5/Geode5Recurrence.lean "$dst/Recurrence.lean"
+          cp controller/proofs/geode5/data/G5_1000.txt "$dst/data/G5_1000.txt"
+          cp controller/proofs/geode5/data/residues_480.txt "$dst/data/residues_480.txt"
+          test -z "$(grep -nE '\b(sorry|admit)\b' \
+            "$dst/CRT.lean" "$dst/MomentAlgebra.lean" \
+            "$dst/Integral.lean" "$dst/Recurrence.lean" || true)"
+
+      - name: Install Lean 4.27
+        shell: bash
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          "$HOME/.elan/bin/elan" toolchain install leanprover/lean4:v4.27.0
+
+      - name: Fetch Mathlib cache
+        working-directory: target
+        run: lake exe cache get
+
+      - name: Compile symbolic moment algebra
+        working-directory: target
+        shell: bash
+        run: |
+          set -o pipefail
+          lake env lean -DwarningAsError=true \
+            FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentAlgebra.lean \
+            2>&1 | tee geode5-moment-audit.log
+
+      - name: Compile algebraic integral layer
+        working-directory: target
+        shell: bash
+        run: |
+          set -o pipefail
+          lake env lean -DwarningAsError=true \
+            FormalConjectures/Arxiv/2508.10245/Geode5Proof/Integral.lean \
+            2>&1 | tee geode5-integral-audit.log
+
+      - name: Compile exact moment recurrence
+        working-directory: target
+        shell: bash
+        run: |
+          set -o pipefail
+          lake env lean -DwarningAsError=true \
+            FormalConjectures/Arxiv/2508.10245/Geode5Proof/Recurrence.lean \
+            2>&1 | tee geode5-recurrence-audit.log
+
+      - name: Compile CRT certificate
+        working-directory: target
+        shell: bash
+        run: |
+          set -o pipefail
+          lake env lean -DwarningAsError=true \
+            FormalConjectures/Arxiv/2508.10245/Geode5Proof/CRT.lean \
+            2>&1 | tee geode5-crt-audit.log
+
+      - name: Upload compiler transcripts
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: geode5-proof-audit
+          path: |
+            target/geode5-moment-audit.log
+            target/geode5-integral-audit.log
+            target/geode5-recurrence-audit.log
+            target/geode5-crt-audit.log
+          if-no-files-found: warn

proofs/geode5/Geode5CRT.lean

@@ -0,0 +1,141 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Arxiv.«2508.10245».Geode5
+import Mathlib.Data.Nat.ChineseRemainder
+
+/-!
+# CRT certificate layer for the five-dimensional Geode computation
+
+This module formalizes the exact Chinese-remainder and uniqueness layer from the
+computational certificate for `G(1000,1000,1000,1000,1000)`.
+
+It deliberately separates the already-checkable arithmetic certificate from the
+remaining mathematical bridge: proving that the five-state moment recurrence
+computes `geode5Diagonal`.
+-/
+
+namespace Arxiv.«2508.10245».Geode5Proof
+
+open scoped Function
+
+private def parseNat (s : String) : ℕ :=
+  s.trim.toNat?.getD 0
+
+private def parsePair (line : String) : ℕ × ℕ :=
+  match line.trim.splitOn " " with
+  | p :: r :: _ => (parseNat p, parseNat r)
+  | _ => (0, 0)
+
+/-- The exact 8,367-digit candidate value from the certificate package. -/
+def answerValue : ℕ :=
+  parseNat (include_str "data/G5_1000.txt")
+
+/-- The rigorous hyper-Catalan upper bound used in the certificate. -/
+def upperBound : ℕ :=
+  Nat.factorial 20002 /
+    (Nat.factorial 15002 * Nat.factorial 1001 * Nat.factorial 1000 ^ 4)
+
+/-- The 480 `(prime, residue)` pairs used for the CRT reconstruction. -/
+def residuePairs : List (ℕ × ℕ) :=
+  ((include_str "data/residues_480.txt").trim.splitOn "\n").map parsePair
+
+/-- Product of all 480 moduli. -/
+def certificateModulus : ℕ := (residuePairs.map Prod.fst).prod
+
+theorem residuePairs_length : residuePairs.length = 480 := by
+  native_decide
+
+/-- The stored moduli are pairwise coprime. -/
+theorem residueModuli_pairwise_coprime :
+    residuePairs.Pairwise (Nat.Coprime on Prod.fst) := by
+  native_decide
+
+/-- Every stored residue is in the canonical interval for its modulus. -/
+theorem residueValues_canonical :
+    ∀ pr ∈ residuePairs, pr.2 < pr.1 := by
+  native_decide
+
+/-- The proposed exact answer has every residue recorded in the ZIP certificate. -/
+theorem answer_modEq_residue :
+    ∀ pr ∈ residuePairs, answerValue ≡ pr.2 [MOD pr.1] := by
+  native_decide
+
+/-- The hyper-Catalan upper bound is strictly below the CRT modulus. -/
+theorem upperBound_lt_certificateModulus :
+    upperBound < certificateModulus := by
+  native_decide
+
+/-- The proposed answer lies below the rigorous upper bound. -/
+theorem answerValue_lt_upperBound : answerValue < upperBound := by
+  native_decide
+
+/--
+Any natural number with the 480 certified residues is congruent to `answerValue`
+modulo the product of all 480 moduli.
+-/
+theorem modEq_answerValue_of_residues (z : ℕ)
+    (hz : ∀ pr ∈ residuePairs, z ≡ pr.2 [MOD pr.1]) :
+    z ≡ answerValue [MOD certificateModulus] := by
+  apply (Nat.modEq_list_map_prod_iff residueModuli_pairwise_coprime).2
+  intro pr hpr
+  exact (hz pr hpr).trans (answer_modEq_residue pr hpr).symm
+
+/--
+CRT uniqueness below the rigorous Geode upper bound.
+
+This is the final arithmetic step of the certificate: once a nonnegative
+candidate is proved to satisfy the stored residues and the hyper-Catalan bound,
+it must equal the 8,367-digit answer.
+-/
+theorem eq_answerValue_of_residues_of_lt_upperBound (z : ℕ)
+    (hz : ∀ pr ∈ residuePairs, z ≡ pr.2 [MOD pr.1])
+    (hzlt : z < upperBound) :
+    z = answerValue := by
+  exact (modEq_answerValue_of_residues z hz).eq_of_lt_of_lt
+    (hzlt.trans upperBound_lt_certificateModulus)
+    (answerValue_lt_upperBound.trans upperBound_lt_certificateModulus)
+
+/--
+The exact remaining bridge needed to discharge the benchmark theorem from the
+ZIP certificate.
+
+The recurrence formalization must supply:
+1. nonnegativity of `geode5Diagonal 1000`;
+2. the hyper-Catalan upper bound;
+3. all 480 modular residue equalities.
+-/
+theorem geode5_1000_of_certificate
+    (hnonneg : 0 ≤ geode5Diagonal 1000)
+    (hbound : Int.toNat (geode5Diagonal 1000) < upperBound)
+    (hres : ∀ pr ∈ residuePairs,
+      Int.toNat (geode5Diagonal 1000) ≡ pr.2 [MOD pr.1]) :
+    geode5Diagonal 1000 = (answerValue : ℤ) := by
+  have hnat :
+      Int.toNat (geode5Diagonal 1000) = answerValue :=
+    eq_answerValue_of_residues_of_lt_upperBound _ hres hbound
+  calc
+    geode5Diagonal 1000 = Int.toNat (geode5Diagonal 1000) := by
+      symm
+      exact Int.toNat_of_nonneg hnonneg
+    _ = answerValue := by exact_mod_cast hnat
+
+#print axioms residueModuli_pairwise_coprime
+#print axioms answer_modEq_residue
+#print axioms upperBound_lt_certificateModulus
+#print axioms geode5_1000_of_certificate
+
+end Arxiv.«2508.10245».Geode5Proof

proofs/geode5/Geode5CastBridges.lean

@@ -0,0 +1,82 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.HyperCatalanIntegrality
+
+/-!
+# Cast bridges from the benchmark definition to the rational Geode proof
+-/
+
+namespace Arxiv.«2508.10245».Geode5Proof
+
+open scoped BigOperators
+
+inductive FourLetter
+  | first | second | third | fourth
+  deriving DecidableEq, Fintype
+
+/-- Four symbol multiplicities used for the ordinary multinomial coefficient. -/
+def fourCounts (a b c d : ℕ) : FourLetter → ℕ
+  | .first => a
+  | .second => b
+  | .third => c
+  | .fourth => d
+
+/-- The denominator in `multinomial4` divides its factorial numerator. -/
+theorem multinomial4_denominator_dvd (a b c d : ℕ) :
+    Nat.factorial a * Nat.factorial b * Nat.factorial c * Nat.factorial d ∣
+      Nat.factorial (a + b + c + d) := by
+  simpa [fourCounts, mul_assoc, add_assoc, add_comm, add_left_comm] using
+    (Nat.prod_factorial_dvd_factorial_sum Finset.univ (fourCounts a b c d))
+
+/-- Cast of `multinomial4` equals the exact rational factorial quotient. -/
+theorem cast_multinomial4_eq_qMultinomial4 (a b c d : ℕ) :
+    (multinomial4 a b c d : ℚ) = qMultinomial4 a b c d := by
+  rw [multinomial4, Nat.cast_div (multinomial4_denominator_dvd a b c d)]
+  simp [qMultinomial4, qFactorial]
+
+/-- Rational version of the original alternating-sum definition. -/
+def qGeode5Diagonal (n : ℕ) : ℚ :=
+  ∑ j₂ ∈ Finset.range (n + 1),
+    ∑ j₃ ∈ Finset.range (n + 1),
+      ∑ j₄ ∈ Finset.range (n + 1),
+        ∑ j₅ ∈ Finset.range (n + 1),
+          (-1 : ℚ) ^ (j₂ + j₃ + j₄ + j₅) *
+            qMultinomial4 j₂ j₃ j₄ j₅ *
+              qHyperCatalan5 (n + 1 + j₂ + j₃ + j₄ + j₅)
+                (n - j₂) (n - j₃) (n - j₄) (n - j₅)
+
+/-- Casting the exact benchmark definition gives the rational alternating sum. -/
+theorem cast_geode5Diagonal_eq_qGeode5Diagonal (n : ℕ) :
+    (geode5Diagonal n : ℚ) = qGeode5Diagonal n := by
+  simp only [geode5Diagonal, qGeode5Diagonal, Int.cast_sum, Int.cast_mul,
+    Int.cast_pow, Int.cast_neg, Int.cast_one, Nat.cast_ofNat]
+  apply Finset.sum_congr rfl
+  intro j₂ hj₂
+  apply Finset.sum_congr rfl
+  intro j₃ hj₃
+  apply Finset.sum_congr rfl
+  intro j₄ hj₄
+  apply Finset.sum_congr rfl
+  intro j₅ hj₅
+  rw [cast_multinomial4_eq_qMultinomial4,
+    cast_hyperCatalan5_eq_qHyperCatalan5]
+  norm_num
+
+#print axioms cast_multinomial4_eq_qMultinomial4
+#print axioms cast_geode5Diagonal_eq_qGeode5Diagonal
+
+end Arxiv.«2508.10245».Geode5Proof