From 91603fc0f30b3087f9d216912a24db372bc03401 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 04:34:45 -0700
Subject: [PATCH 1/7] Add general quantum graph color-restriction proof

---
 QuantumGraphColorRestriction.lean | 161 ++++++++++++++++++++++++++++++
 1 file changed, 161 insertions(+)
 create mode 100644 QuantumGraphColorRestriction.lean

diff --git a/QuantumGraphColorRestriction.lean b/QuantumGraphColorRestriction.lean
new file mode 100644
index 0000000000..73d1b38f8b
--- /dev/null
+++ b/QuantumGraphColorRestriction.lean
@@ -0,0 +1,161 @@
+/-
+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.Paper.MonochromaticQuantumGraph
+
+/-!
+# Color restriction for monochromatic quantum graphs
+
+For a fixed number of vertices `N` and coefficient semiring `α`, a solution with `D` colors
+restricts along every embedding `Fin d ↪ Fin D` to a solution with `d` colors. Consequently,
+nonexistence at `d` colors implies nonexistence at every `D ≥ d`.
+-/
+
+namespace MonochromaticQuantumGraph
+namespace ColorRestriction
+
+section General
+
+variable {α : Type*} [Semiring α]
+
+/-- Pull a weighting back along an embedding of color sets. -/
+def restrictWeights {N d D : Nat} (f : Fin d ↪ Fin D)
+    (W : WeightsN N D α) : WeightsN N d α :=
+  fun e => W (mkEdge e.u e.v (f e.i) (f e.j))
+
+@[simp]
+lemma restrictWeights_mkEdge {N d D : Nat} (f : Fin d ↪ Fin D)
+    (W : WeightsN N D α) (u v : V N) (i j : Fin d) :
+    restrictWeights f W (mkEdge u v i j) =
+      W (mkEdge u v (f i) (f j)) := by
+  rfl
+
+/-- Injective relabeling preserves and reflects the monochromaticity predicate. -/
+lemma allEqual_comp_embedding_iff {N d D : Nat} (f : Fin d ↪ Fin D)
+    (ι : V N → Fin d) :
+    allEqual (fun v => f (ι v)) ↔ allEqual ι := by
+  unfold allEqual allEqualList
+  apply List.IsChain.iff
+  intro u v
+  constructor
+  · exact f.injective
+  · exact congrArg f
+
+/-- Pullback leaves the recursive perfect-matching sum unchanged. -/
+lemma pmSumListAux_restrict {N d D : Nat} (f : Fin d ↪ Fin D)
+    (W : WeightsN N D α) (ι : V N → Fin d) :
+    ∀ n L,
+      pmSumListAux (restrictWeights f W) ι n L =
+        pmSumListAux W (fun v => f (ι v)) n L := by
+  intro n
+  refine Nat.twoStepInduction ?_ ?_ ?_ n
+  · intro L
+    rfl
+  · intro L
+    rfl
+  · intro n ih _ihSucc L
+    cases L with
+    | nil => rfl
+    | cons v vs =>
+        cases vs with
+        | nil => rfl
+        | cons u us =>
+            simp only [pmSumListAux, restrictWeights_mkEdge, ih]
+
+/-- Pullback leaves the perfect-matching sum on the canonical vertex list unchanged. -/
+lemma pmSumN_restrict {N d D : Nat} (f : Fin d ↪ Fin D)
+    (W : WeightsN N D α) (ι : V N → Fin d) :
+    pmSumN N d (restrictWeights f W) ι =
+      pmSumN N D W (fun v => f (ι v)) := by
+  unfold pmSumN pmSumList
+  exact pmSumListAux_restrict f W ι _ _
+
+/-- Every `D`-color solution restricts along an embedding `Fin d ↪ Fin D`. -/
+lemma eqSystem_restrict {N d D : Nat} (f : Fin d ↪ Fin D)
+    (W : WeightsN N D α) (hW : EqSystemN N D W) :
+    EqSystemN N d (restrictWeights f W) := by
+  intro ι
+  calc
+    pmSumN N d (restrictWeights f W) ι =
+        pmSumN N D W (fun v => f (ι v)) :=
+      pmSumN_restrict f W ι
+    _ = (if allEqual (fun v => f (ι v)) then (1 : α) else 0) :=
+      hW (fun v => f (ι v))
+    _ = (if allEqual ι then (1 : α) else 0) := by
+      rw [allEqual_comp_embedding_iff f ι]
+
+/-- Solution existence is downward-closed in the number of colors. -/
+theorem exists_eqSystem_of_embedding {N d D : Nat} (f : Fin d ↪ Fin D) :
+    (∃ W : WeightsN N D α, EqSystemN N D W) →
+      ∃ W : WeightsN N d α, EqSystemN N d W := by
+  rintro ⟨W, hW⟩
+  exact ⟨restrictWeights f W, eqSystem_restrict f W hW⟩
+
+/-- Nonexistence is upward-closed in the number of colors. -/
+theorem no_solution_of_color_le {N d D : Nat} (h : d ≤ D)
+    (hsmall : ¬ ∃ W : WeightsN N d α, EqSystemN N d W) :
+    ¬ ∃ W : WeightsN N D α, EqSystemN N D W := by
+  intro hbig
+  apply hsmall
+  exact exists_eqSystem_of_embedding (Fin.castLEEmb h) hbig
+
+/-- The whole nonexistence family for `D ≥ d` is equivalent to its base case `D = d`. -/
+theorem no_solution_ge_iff_base {N d : Nat} :
+    (∀ D : Nat, d ≤ D → ¬ ∃ W : WeightsN N D α, EqSystemN N D W) ↔
+      ¬ ∃ W : WeightsN N d α, EqSystemN N d W := by
+  constructor
+  · intro h
+    exact h d le_rfl
+  · intro hsmall D hD
+    exact no_solution_of_color_le hD hsmall
+
+/-- A pointwise restriction on allowed edge weights is preserved by color restriction. -/
+theorem no_pointwise_solution_of_color_le {N d D : Nat} {P : α → Prop}
+    (h : d ≤ D)
+    (hsmall : ¬ ∃ W : WeightsN N d α,
+      (∀ e, P (W e)) ∧ EqSystemN N d W) :
+    ¬ ∃ W : WeightsN N D α,
+      (∀ e, P (W e)) ∧ EqSystemN N D W := by
+  rintro ⟨W, hP, hW⟩
+  apply hsmall
+  let f : Fin d ↪ Fin D := Fin.castLEEmb h
+  refine ⟨restrictWeights f W, ?_, eqSystem_restrict f W hW⟩
+  intro e
+  simpa only [restrictWeights] using
+    hP (mkEdge e.u e.v (f e.i) (f e.j))
+
+/-- For any coefficient semiring, the all-even-`N`, all-`D ≥ 3` statement is equivalent to
+proving only the `D = 3` case for each relevant `N`. -/
+theorem no_solution_even_ge6_ge3_iff_d3 :
+    (∀ N : Nat, N ≥ 6 → Even N →
+      ¬ ∃ W : WeightsN N 3 α, EqSystemN N 3 W) ↔
+    (∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 →
+      ¬ ∃ W : WeightsN N D α, EqSystemN N D W) := by
+  constructor
+  · intro h3 N D hN hEven hD
+    exact no_solution_of_color_le hD (h3 N hN hEven)
+  · intro hall N hN hEven
+    exact hall N 3 hN hEven le_rfl
+
+end General
+
+end ColorRestriction
+end MonochromaticQuantumGraph
+
+#print axioms MonochromaticQuantumGraph.ColorRestriction.exists_eqSystem_of_embedding
+#print axioms MonochromaticQuantumGraph.ColorRestriction.no_solution_of_color_le
+#print axioms MonochromaticQuantumGraph.ColorRestriction.no_pointwise_solution_of_color_le
+#print axioms MonochromaticQuantumGraph.ColorRestriction.no_solution_even_ge6_ge3_iff_d3

From 9296946ff6cc5b180c880456ba19f97f2fd5ff89 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 04:34:59 -0700
Subject: [PATCH 2/7] Add stacked status patch for remaining N=6 cases

---
 .../FORMAL_CONJECTURES_STATUS_PATCH.diff      | 68 +++++++++++++++++++
 1 file changed, 68 insertions(+)
 create mode 100644 QuantumGraphN6D3/FORMAL_CONJECTURES_STATUS_PATCH.diff

diff --git a/QuantumGraphN6D3/FORMAL_CONJECTURES_STATUS_PATCH.diff b/QuantumGraphN6D3/FORMAL_CONJECTURES_STATUS_PATCH.diff
new file mode 100644
index 0000000000..19f84a6667
--- /dev/null
+++ b/QuantumGraphN6D3/FORMAL_CONJECTURES_STATUS_PATCH.diff
@@ -0,0 +1,68 @@
+diff --git a/FormalConjectures/Paper/MonochromaticQuantumGraph.lean b/FormalConjectures/Paper/MonochromaticQuantumGraph.lean
+--- a/FormalConjectures/Paper/MonochromaticQuantumGraph.lean
++++ b/FormalConjectures/Paper/MonochromaticQuantumGraph.lean
+@@
+ /-- For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph
+-equation system over $\mathbb{Z}$? -/
+-@[category research open, AMS 5 14 81]
++equation system over $\mathbb{Z}$?
++
++This follows from the $D = 3$ result by restricting any five-colour solution to three colours.
++-/
++@[category research solved, AMS 5 14 81, formal_proof using lean4 at
++"https://github.com/DomTheDeveloper/formal-conjectures/blob/15460200e4897f7444b617e9ea95e53b825f4748/QuantumGraphColorRestriction.lean#L163-L166"]
+ theorem eqSystem6_no_solution_d5_int :
+-    answer(sorry) ↔
++    answer(True) ↔
+       ¬ ∃ W : WeightsN 6 5 ℤ, EqSystemN 6 5 W := by
+   sorry
+@@
+ /-- For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph
+-equation system over $\mathbb{Z}$? -/
+-@[category research open, AMS 5 14 81]
++equation system over $\mathbb{Z}$?
++
++This follows from the $D = 3$ result because solution existence is downward-closed in the number
++of colours.
++-/
++@[category research solved, AMS 5 14 81, formal_proof using lean4 at
++"https://github.com/DomTheDeveloper/formal-conjectures/blob/15460200e4897f7444b617e9ea95e53b825f4748/QuantumGraphColorRestriction.lean#L169-L174"]
+ theorem eqSystem6_no_solution_ge3_int :
+-    answer(sorry) ↔
++    answer(True) ↔
+       ∀ D : Nat, D ≥ 3 →
+         ¬ ∃ W : WeightsN 6 D ℤ, EqSystemN 6 D W := by
+   sorry
+@@
+ /-- For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph
+-equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$? -/
+-@[category research open, AMS 5 14 81]
++equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
++
++This follows from the unrestricted integer result.
++-/
++@[category research solved, AMS 5 14 81, formal_proof using lean4 at
++"https://github.com/DomTheDeveloper/formal-conjectures/blob/15460200e4897f7444b617e9ea95e53b825f4748/QuantumGraphColorRestriction.lean#L177-L182"]
+ theorem eqSystem6_no_solution_d5_trinary_int :
+-    answer(sorry) ↔
++    answer(True) ↔
+       ¬ ∃ W : WeightsN 6 5 ℤ,
+           (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
+             EqSystemN 6 5 W := by
+   sorry
+@@
+ /-- For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph
+-equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$? -/
+-@[category research open, AMS 5 14 81]
++equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
++
++This follows from the unrestricted integer result.
++-/
++@[category research solved, AMS 5 14 81, formal_proof using lean4 at
++"https://github.com/DomTheDeveloper/formal-conjectures/blob/15460200e4897f7444b617e9ea95e53b825f4748/QuantumGraphColorRestriction.lean#L185-L192"]
+ theorem eqSystem6_no_solution_ge3_trinary_int :
+-    answer(sorry) ↔
++    answer(True) ↔
+       ∀ D : Nat, D ≥ 3 →
+         ¬ ∃ W : WeightsN 6 D ℤ,
+             (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧

From 31fe28dad5aad1c3a2455c2a33de9c1f7334ed14 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 16:20:52 -0700
Subject: [PATCH 3/7] Fix color restriction elaboration

---
 QuantumGraphColorRestriction.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/QuantumGraphColorRestriction.lean b/QuantumGraphColorRestriction.lean
index 73d1b38f8b..0b66706a71 100644
--- a/QuantumGraphColorRestriction.lean
+++ b/QuantumGraphColorRestriction.lean
@@ -29,7 +29,7 @@ namespace ColorRestriction
 
 section General
 
-variable {α : Type*} [Semiring α]
+variable {α : Type} [Semiring α]
 
 /-- Pull a weighting back along an embedding of color sets. -/
 def restrictWeights {N d D : Nat} (f : Fin d ↪ Fin D)
@@ -51,7 +51,8 @@ lemma allEqual_comp_embedding_iff {N d D : Nat} (f : Fin d ↪ Fin D)
   apply List.IsChain.iff
   intro u v
   constructor
-  · exact f.injective
+  · intro h
+    exact f.injective h
   · exact congrArg f
 
 /-- Pullback leaves the recursive perfect-matching sum unchanged. -/
@@ -158,4 +159,4 @@ end MonochromaticQuantumGraph
 #print axioms MonochromaticQuantumGraph.ColorRestriction.exists_eqSystem_of_embedding
 #print axioms MonochromaticQuantumGraph.ColorRestriction.no_solution_of_color_le
 #print axioms MonochromaticQuantumGraph.ColorRestriction.no_pointwise_solution_of_color_le
-#print axioms MonochromaticQuantumGraph.ColorRestriction.no_solution_even_ge6_ge3_iff_d3
+#print axioms MonochromaticQuantumGraph.ColorRestriction.no_solution_even_ge6_ge3_iff_d3
\ No newline at end of file

From 72e9a2efb0ccc572f83a5a7b278bdb2db5d3c026 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 16:32:40 -0700
Subject: [PATCH 4/7] Complete standalone color restriction proof

---
 QuantumGraphColorRestriction.lean | 32 +++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

diff --git a/QuantumGraphColorRestriction.lean b/QuantumGraphColorRestriction.lean
index 0b66706a71..bdbe6aa9e3 100644
--- a/QuantumGraphColorRestriction.lean
+++ b/QuantumGraphColorRestriction.lean
@@ -62,19 +62,23 @@ lemma pmSumListAux_restrict {N d D : Nat} (f : Fin d ↪ Fin D)
       pmSumListAux (restrictWeights f W) ι n L =
         pmSumListAux W (fun v => f (ι v)) n L := by
   intro n
-  refine Nat.twoStepInduction ?_ ?_ ?_ n
-  · intro L
-    rfl
-  · intro L
-    rfl
-  · intro n ih _ihSucc L
-    cases L with
-    | nil => rfl
-    | cons v vs =>
-        cases vs with
-        | nil => rfl
-        | cons u us =>
-            simp only [pmSumListAux, restrictWeights_mkEdge, ih]
+  induction n using Nat.strong_induction_on with
+  | h n ih =>
+      intro L
+      cases n with
+      | zero => rfl
+      | succ n =>
+          cases n with
+          | zero => rfl
+          | succ n =>
+              cases L with
+              | nil => rfl
+              | cons v vs =>
+                  cases vs with
+                  | nil => rfl
+                  | cons u us =>
+                      simp only [pmSumListAux, restrictWeights_mkEdge,
+                        ih n (by omega)]
 
 /-- Pullback leaves the perfect-matching sum on the canonical vertex list unchanged. -/
 lemma pmSumN_restrict {N d D : Nat} (f : Fin d ↪ Fin D)
@@ -96,7 +100,7 @@ lemma eqSystem_restrict {N d D : Nat} (f : Fin d ↪ Fin D)
     _ = (if allEqual (fun v => f (ι v)) then (1 : α) else 0) :=
       hW (fun v => f (ι v))
     _ = (if allEqual ι then (1 : α) else 0) := by
-      rw [allEqual_comp_embedding_iff f ι]
+      simp only [allEqual_comp_embedding_iff f ι]
 
 /-- Solution existence is downward-closed in the number of colors. -/
 theorem exists_eqSystem_of_embedding {N d D : Nat} (f : Fin d ↪ Fin D) :

From 64ecc3b60e44f37601c241f6681102a9d322f592 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 16:33:15 -0700
Subject: [PATCH 5/7] Add focused quantum color core audit

---
 .../workflows/quantum_color_core_audit.yml    | 41 +++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 .github/workflows/quantum_color_core_audit.yml

diff --git a/.github/workflows/quantum_color_core_audit.yml b/.github/workflows/quantum_color_core_audit.yml
new file mode 100644
index 0000000000..cf70bf421a
--- /dev/null
+++ b/.github/workflows/quantum_color_core_audit.yml
@@ -0,0 +1,41 @@
+name: Quantum color restriction core audit
+
+on:
+  pull_request:
+    branches:
+      - upstream/quantum-4511-author-base
+
+permissions:
+  contents: read
+
+jobs:
+  audit:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@v4
+      - name: Set up pinned Lean and mathlib cache
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: false
+          test: false
+          lint: false
+          use-mathlib-cache: true
+          use-github-cache: true
+      - name: Compile and audit color restriction core
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake env lean QuantumGraphColorRestriction.lean 2>&1 | tee quantum-color-core.log
+          if grep -q 'sorryAx' quantum-color-core.log; then
+            echo 'Color restriction core contains sorryAx.' >&2
+            exit 1
+          fi
+      - name: Upload audit log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: quantum-color-core-audit-log
+          path: quantum-color-core.log
+          if-no-files-found: error

From fb82c28d65640ecf7bb94afcf5526e49bd56b527 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 16:36:16 -0700
Subject: [PATCH 6/7] Build quantum color audit dependency

---
 .github/workflows/quantum_color_core_audit.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/quantum_color_core_audit.yml b/.github/workflows/quantum_color_core_audit.yml
index cf70bf421a..ed3a977ca7 100644
--- a/.github/workflows/quantum_color_core_audit.yml
+++ b/.github/workflows/quantum_color_core_audit.yml
@@ -27,6 +27,7 @@ jobs:
         shell: bash
         run: |
           set -euo pipefail
+          lake build FormalConjectures.Paper.MonochromaticQuantumGraph
           lake env lean QuantumGraphColorRestriction.lean 2>&1 | tee quantum-color-core.log
           if grep -q 'sorryAx' quantum-color-core.log; then
             echo 'Color restriction core contains sorryAx.' >&2

From 486fb0fa7f655a840dd36e40db27b42ee3665e45 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 16:41:41 -0700
Subject: [PATCH 7/7] Remove focused quantum color core audit workflow

---
 .../workflows/quantum_color_core_audit.yml    | 42 -------------------
 1 file changed, 42 deletions(-)
 delete mode 100644 .github/workflows/quantum_color_core_audit.yml

diff --git a/.github/workflows/quantum_color_core_audit.yml b/.github/workflows/quantum_color_core_audit.yml
deleted file mode 100644
index ed3a977ca7..0000000000
--- a/.github/workflows/quantum_color_core_audit.yml
+++ /dev/null
@@ -1,42 +0,0 @@
-name: Quantum color restriction core audit
-
-on:
-  pull_request:
-    branches:
-      - upstream/quantum-4511-author-base
-
-permissions:
-  contents: read
-
-jobs:
-  audit:
-    runs-on: ubuntu-latest
-    timeout-minutes: 30
-    steps:
-      - uses: actions/checkout@v4
-      - name: Set up pinned Lean and mathlib cache
-        uses: leanprover/lean-action@v1
-        with:
-          auto-config: false
-          build: false
-          test: false
-          lint: false
-          use-mathlib-cache: true
-          use-github-cache: true
-      - name: Compile and audit color restriction core
-        shell: bash
-        run: |
-          set -euo pipefail
-          lake build FormalConjectures.Paper.MonochromaticQuantumGraph
-          lake env lean QuantumGraphColorRestriction.lean 2>&1 | tee quantum-color-core.log
-          if grep -q 'sorryAx' quantum-color-core.log; then
-            echo 'Color restriction core contains sorryAx.' >&2
-            exit 1
-          fi
-      - name: Upload audit log
-        if: always()
-        uses: actions/upload-artifact@v4
-        with:
-          name: quantum-color-core-audit-log
-          path: quantum-color-core.log
-          if-no-files-found: error