From fe341ca95abb64c294569555537356e472f3a76d Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 04:11:54 -0700 Subject: [PATCH 1/4] Prove color restriction and N=6 integer consequences --- QuantumGraphColorRestriction.lean | 188 ++++++++++++++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 QuantumGraphColorRestriction.lean diff --git a/QuantumGraphColorRestriction.lean b/QuantumGraphColorRestriction.lean new file mode 100644 index 0000000000..8e8e5a438f --- /dev/null +++ b/QuantumGraphColorRestriction.lean @@ -0,0 +1,188 @@ +import QuantumGraphGlobal + +/-! +# 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`. + +The final four theorems combine this structural reduction with the independently checked +`N = 6`, `D = 3` integer obstruction in `QuantumGraphGlobal`. +-/ + +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 + +section N6IntegerConsequences + +/-- The `N = 6`, `D = 5` unrestricted integer obstruction. -/ +theorem no_eqSystem6_d5_int : + ¬ ∃ W : WeightsN 6 5 ℤ, EqSystemN 6 5 W := by + exact no_solution_of_color_le (α := ℤ) (N := 6) (d := 3) (D := 5) + (by omega) QuantumGraphGlobal.no_eqSystem_int + +/-- The unrestricted integer obstruction for every `D ≥ 3`. -/ +theorem no_eqSystem6_ge3_int : + ∀ D : Nat, D ≥ 3 → + ¬ ∃ W : WeightsN 6 D ℤ, EqSystemN 6 D W := by + intro D hD + exact no_solution_of_color_le (α := ℤ) (N := 6) (d := 3) (D := D) + hD QuantumGraphGlobal.no_eqSystem_int + +/-- The `D = 5` trinary obstruction. -/ +theorem no_eqSystem6_d5_trinary_int : + ¬ ∃ W : WeightsN 6 5 ℤ, + (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧ + EqSystemN 6 5 W := by + rintro ⟨W, _, hW⟩ + exact no_eqSystem6_d5_int ⟨W, hW⟩ + +/-- The trinary obstruction for every `D ≥ 3`. -/ +theorem no_eqSystem6_ge3_trinary_int : + ∀ D : Nat, D ≥ 3 → + ¬ ∃ W : WeightsN 6 D ℤ, + (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧ + EqSystemN 6 D W := by + intro D hD + rintro ⟨W, _, hW⟩ + exact no_eqSystem6_ge3_int D hD ⟨W, hW⟩ + +end N6IntegerConsequences + +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 +#print axioms MonochromaticQuantumGraph.ColorRestriction.no_eqSystem6_d5_int +#print axioms MonochromaticQuantumGraph.ColorRestriction.no_eqSystem6_ge3_int +#print axioms MonochromaticQuantumGraph.ColorRestriction.no_eqSystem6_d5_trinary_int +#print axioms MonochromaticQuantumGraph.ColorRestriction.no_eqSystem6_ge3_trinary_int From 91d23c06cbb5936e494130c499e99f5b25ad7fdd Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 04:16:06 -0700 Subject: [PATCH 2/4] Trigger corrected full quantum color-restriction audit --- QuantumGraphN6D3/COLOR_RESTRICTION_AUDIT.md | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 QuantumGraphN6D3/COLOR_RESTRICTION_AUDIT.md diff --git a/QuantumGraphN6D3/COLOR_RESTRICTION_AUDIT.md b/QuantumGraphN6D3/COLOR_RESTRICTION_AUDIT.md new file mode 100644 index 0000000000..59afcfddb5 --- /dev/null +++ b/QuantumGraphN6D3/COLOR_RESTRICTION_AUDIT.md @@ -0,0 +1,5 @@ +# Color-restriction audit + +This branch extends the complete `N = 6`, `D = 3` certificate proof with a coefficient-independent color-restriction theorem and the `D = 5` / all-`D ≥ 3` integer and trinary consequences. + +The focused pull-request workflow downloads and hash-checks the 47 LRAT certificates, replays `verify.sh`, compiles `QuantumGraphColorRestriction.lean` with the certificate directory on `LEAN_PATH`, prints the terminal theorem axioms, and rejects `sorryAx`. From 15460200e4897f7444b617e9ea95e53b825f4748 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 04:17:48 -0700 Subject: [PATCH 3/4] Add Formal Conjectures copyright header --- QuantumGraphColorRestriction.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/QuantumGraphColorRestriction.lean b/QuantumGraphColorRestriction.lean index 8e8e5a438f..eba7716325 100644 --- a/QuantumGraphColorRestriction.lean +++ b/QuantumGraphColorRestriction.lean @@ -1,3 +1,19 @@ +/- +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 QuantumGraphGlobal /-! From b581cc23656fd73c23619fc5205e859cf475a8cd Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 04:33:46 -0700 Subject: [PATCH 4/4] Add Formal Conjectures status patch for all N=6 integer colors --- .../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) ∧