1. FormalConjectures
  2. Paper
  3. MonochromaticQuantumGraph
/- 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 FormalConjecturesUtil

Monochromatic quantum graphs (inherited vertex colorings)

This file studies the existence of monochromatic quantum graphs: edge-coloured, edge-weighted complete graphs whose perfect matchings induce vertex colourings, with the property that

    every non-monochromatic inherited vertex colouring has total weight 0, while

    each of the D monochromatic colourings has total weight 1.

In the quantum-optics motivation, such a construction corresponds to generating high-dimensional multipartite GHZ-type states using probabilistic pair sources and linear optics (without additional resources), where interference patterns can be expressed as weighted sums over perfect matchings.

Main questions (informal)

    For N = 4 and D ≥ 4, does there exist such a graph/weighting?

    For even N ≥ 6 and D ≥ 3, does there exist such a graph/weighting?

Formalisation sketch

A quantum graph with N vertices and D colours can be encoded by a weight function W : EdgeN N D α → α (for a coefficient domain α).

For each assignment of vertex indices ι : V N → Fin D, we define a perfect-matching sum pmSumN N D W ι (a sum over perfect matchings, where each matching contributes the product of the corresponding edge weights determined by ι). The equation system EqSystemN N D W requires

pmSumN N D W ι = 1 iff ι is constant (all entries equal), and 0 otherwise.

The open conjectures in this file ask for non-existence/existence of such W over various coefficient domains (e.g. ℂ, ℝ, ℤ, and restricted integer weights).

References

open scoped Matrixopen scoped NNRealnamespace MonochromaticQuantumGraph

Vertices of $K_N$.

abbrev V (N : Nat) := Fin N

Edge label for $K_N$ with endpoint indices in Fin D.

We intend to build edges only with u < v (so undirected edges are represented once), and our enumeration always pairs the first vertex in an ordered list with a later vertex.

structure EdgeN (N D : Nat) where u : V N v : V N i : Fin D j : Fin D deriving DecidableEq

Weights on edges.

abbrev WeightsN (N D : Nat) (α : Type) := EdgeN N D → α

Helper: build an EdgeN from endpoints and endpoint indices.

def mkEdge {N D : Nat} (u v : V N) (i j : Fin D) : EdgeN N D := ⟨u, v, i, j⟩

Ordered vertex list $[0, 1, \ldots, N-1]$.

def vertices : (N : Nat) → List (V N) | 0 => [] | N + 1 => (0 : Fin (N + 1)) :: (vertices N).map Fin.succ

Chain-equality along a list of vertices.

def allEqualList {N D : Nat} (ι : V N → Fin D) (L : List (V N)) : Prop := List.IsChain (fun v w => ι v = ι w) L

All indices equal on Fin N (using the canonical ordered vertex list).

def allEqual {N D : Nat} (ι : V N → Fin D) : Prop := allEqualList ι (vertices N)

Instance: allEqualList ι L is decidable.

instance {N D : Nat} (ι : V N → Fin D) (L : List (V N)) : Decidable (allEqualList ι L) := N:ℕD:ℕι:V N → Fin DL:List (V N)⊢ Decidable (allEqualList ι L) N:ℕD:ℕι:V N → Fin DL:List (V N)this:DecidableRel fun v w ↦ ι v = ι w := fun v w ↦ inferInstance⊢ Decidable (allEqualList ι L) N:ℕD:ℕι:V N → Fin DL:List (V N)this:DecidableRel fun v w ↦ ι v = ι w := fun v w ↦ inferInstance⊢ Decidable (List.IsChain (fun v w ↦ ι v = ι w) L) All goals completed! 🐙

Instance: allEqual ι is decidable.

instance {N D : Nat} (ι : V N → Fin D) : Decidable (allEqual ι) := N:ℕD:ℕι:V N → Fin D⊢ Decidable (allEqual ι) N:ℕD:ℕι:V N → Fin D⊢ Decidable (allEqualList ι (vertices N)) All goals completed! 🐙

Auxiliary perfect-matching sum on a vertex list, using a fuel parameter n for termination.

When called as pmSumListAux W ι L.length L, this computes the weighted sum over all perfect matchings on the vertices in L. The recursion pairs the head vertex with each later vertex and recurses on the remaining vertices.

For lists of odd length, there are no perfect matchings and the value is 0.

def pmSumListAux {α : Type} [Semiring α] {N D : Nat} (W : WeightsN N D α) (ι : V N → Fin D) : Nat → List (V N) → α | 0, _ => 1 | 1, _ => 0 | _ + 2, [] => 1 | _ + 2, [_] => 0 | n + 2, v :: vs => (vs.map (fun u => W (mkEdge v u (ι v) (ι u)) * pmSumListAux W ι n (vs.erase u) )).sum

Perfect-matching sum on a list: run pmSumListAux with fuel = L.length.

def pmSumList {α : Type} [Semiring α] {N D : Nat} (W : WeightsN N D α) (ι : V N → Fin D) (L : List (V N)) : α := pmSumListAux W ι L.length L

The perfect-matching sum for $K_N$: use the canonical ordered vertex list vertices N.

def pmSumN {α : Type} [Semiring α] (N D : Nat) (W : WeightsN N D α) (ι : V N → Fin D) : α := pmSumList W ι (vertices N)

The monochromatic quantum graph equation system for $K_N$.

For every index assignment $\iota : V_N \to \mathrm{Fin}, D$, the perfect-matching sum equals $1$ if $\iota$ is constant (monochromatic inherited vertex colouring), and equals $0$ otherwise.

def EqSystemN {α : Type} [Semiring α] (N D : Nat) (W : WeightsN N D α) : Prop := ∀ ι : V N → Fin D, pmSumN N D W ι = (if allEqual ι then (1 : α) else (0 : α))

Instance: EqSystemN N D W is decidable when α has decidable equality.

instance instDecidableEqSystemN {N D : Nat} {α : Type} [Semiring α] [DecidableEq α] (W : WeightsN N D α) : Decidable (EqSystemN N D W) := Fintype.decidableForallFintype/- ## N = 4, D = 2 (works over any semiring α): witness & proof -/ section N4_D2variable {α : Type} [Semiring α]def Witness4_d2 : WeightsN 4 2 α := fun e => if e = mkEdge 0 1 0 0 then (1 : α) else if e = mkEdge 2 3 0 0 then (1 : α) else if e = mkEdge 0 2 1 1 then (1 : α) else if e = mkEdge 1 3 1 1 then (1 : α) else (0 : α)

Sanity check over ℕ using native_decide.

@[category test, AMS 5 14 81] private theorem eqSystem4_d2_nat : EqSystemN 4 2 (Witness4_d2 (α := ℕ)) := ⊢ EqSystemN 4 2 Witness4_d2 All goals completed! 🐙α:Typeinst✝:Semiring αι:V 4 → Fin 2h:∀ (a b c d : Fin 2), pmSumN 4 2 Witness4_d2 ![a, b, c, d] = if allEqual ![a, b, c, d] then 1 else 0hι:ι = ![ι 0, ι 1, ι 2, ι 3]⊢ pmSumN 4 2 Witness4_d2 ![ι 0, ι 1, ι 2, ι 3] = if allEqual ![ι 0, ι 1, ι 2, ι 3] then 1 else 0; All goals completed! 🐙end N4_D2/- ## N = 4, D = 3 (works over any semiring α): witness & proof -/ section N4_D3variable {α : Type} [Semiring α]def Witness4_d3 : WeightsN 4 3 α := fun e => if e = mkEdge 0 1 0 0 then (1 : α) else if e = mkEdge 2 3 0 0 then (1 : α) else if e = mkEdge 0 2 1 1 then (1 : α) else if e = mkEdge 1 3 1 1 then (1 : α) else if e = mkEdge 0 3 2 2 then (1 : α) else if e = mkEdge 1 2 2 2 then (1 : α) else (0 : α)

Sanity check over ℕ using native_decide.

@[category test, AMS 5 14 81] private theorem eqSystem4_d3_nat : EqSystemN 4 3 (Witness4_d3 (α := ℕ)) := ⊢ EqSystemN 4 3 Witness4_d3 All goals completed! 🐙α:Typeinst✝:Semiring αι:V 4 → Fin 3h:∀ (a b c d : Fin 3), pmSumN 4 3 Witness4_d3 ![a, b, c, d] = if allEqual ![a, b, c, d] then 1 else 0hι:ι = ![ι 0, ι 1, ι 2, ι 3]⊢ pmSumN 4 3 Witness4_d3 ![ι 0, ι 1, ι 2, ι 3] = if allEqual ![ι 0, ι 1, ι 2, ι 3] then 1 else 0; All goals completed! 🐙end N4_D3/- ## N = 6, D = 2 (works over any semiring α): witness & proof -/ section N6_D2variable {α : Type} [Semiring α]def Witness6_d2 : WeightsN 6 2 α := fun e => if e = mkEdge 0 1 0 0 then (1 : α) else if e = mkEdge 2 3 0 0 then (1 : α) else if e = mkEdge 4 5 0 0 then (1 : α) else if e = mkEdge 0 5 1 1 then (1 : α) else if e = mkEdge 1 2 1 1 then (1 : α) else if e = mkEdge 3 4 1 1 then (1 : α) else (0 : α)

Sanity check over ℕ using native_decide.

@[category test, AMS 5 14 81] private theorem eqSystem6_d2_nat : EqSystemN 6 2 (Witness6_d2 (α := ℕ)) := ⊢ EqSystemN 6 2 Witness6_d2 All goals completed! 🐙α:Typeinst✝:Semiring αι:V 6 → Fin 2h:∀ (a b c d e f : Fin 2), pmSumN 6 2 Witness6_d2 ![a, b, c, d, e, f] = if allEqual ![a, b, c, d, e, f] then 1 else 0hι:ι = ![ι 0, ι 1, ι 2, ι 3, ι 4, ι 5]⊢ pmSumN 6 2 Witness6_d2 ![ι 0, ι 1, ι 2, ι 3, ι 4, ι 5] = if allEqual ![ι 0, ι 1, ι 2, ι 3, ι 4, ι 5] then 1 else 0; All goals completed! 🐙end N6_D2

Bogdanov: for $N = 4$ and all $D \geq 4$, no solution exists over $\mathbb{R}_{\geq 0}$.

@[category research solved, AMS 5 14 81] theorem eqSystem4_no_solution_nnreal_ge4 : ∀ D : Nat, D ≥ 4 → ¬ ∃ W : WeightsN 4 D ℝ≥0, EqSystemN 4 D W := ⊢ ∀ D ≥ 4, ¬∃ W, EqSystemN 4 D W All goals completed! 🐙

Bogdanov: for all even $N \geq 6$ and $D \geq 3$, no solution exists over $\mathbb{R}_{\geq 0}$.

@[category research solved, AMS 5 14 81] theorem eqSystem_no_solution_nnreal_even_ge6_ge3 : ∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 → ¬ ∃ W : WeightsN N D ℝ≥0, EqSystemN N D W := ⊢ ∀ (N D : ℕ), N ≥ 6 → Even N → D ≥ 3 → ¬∃ W, EqSystemN N D W All goals completed! 🐙

For all even $N \geq 4$ and $D = N$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

The DeepMind prover agent has found a formal proof for this statement.

@[category research solved, AMS 5 14 81, formal_proof using formal_conjectures at "https://github.com/google-deepmind/formal-conjectures/blob/af88acbf9da0f26e3e934743a819e986e02f6875/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L1006"] theorem eqSystem_no_solution_even_ge4_d_eq_n_explicit : answer(True) ↔ ∀ N : Nat, N ≥ 4 → Even N → ¬ ∃ W : WeightsN N N ℂ, EqSystemN N N W := ⊢ True ↔ ∀ N ≥ 4, Even N → ¬∃ W, EqSystemN N N W All goals completed! 🐙

For $N = 4$ and $D = 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

This is the $D = N$ case, proved using eqSystem_no_solution_even_ge4_d_eq_n_explicit.

@[category research solved, AMS 5 14 81, formal_proof using formal_conjectures at "https://github.com/google-deepmind/formal-conjectures/blob/af88acbf9da0f26e3e934743a819e986e02f6875/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L1021"] theorem eqSystem4_no_solution_d4 : answer(True) ↔ ¬ ∃ W : WeightsN 4 4 ℂ, EqSystemN 4 4 W := ⊢ True ↔ ¬∃ W, EqSystemN 4 4 W All goals completed! 🐙

For $N = 4$ and all $D \geq 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

The DeepMind prover agent has found a formal proof of this statement.

@[category research solved, AMS 5 14 81, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/4854c7233c58a7dce45fdd58b1826abf2c9c1a0f/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L549"] theorem eqSystem4_no_solution_ge4 : answer(True) ↔ ∀ D : Nat, D ≥ 4 → ¬ ∃ W : WeightsN 4 D ℂ, EqSystemN 4 D W := ⊢ True ↔ ∀ D ≥ 4, ¬∃ W, EqSystemN 4 D W All goals completed! 🐙

For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem6_no_solution_d3 : answer(sorry) ↔ ¬ ∃ W : WeightsN 6 3 ℂ, EqSystemN 6 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 6 3 W All goals completed! 🐙

For $N = 6$ and $D = 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem6_no_solution_d4 : answer(sorry) ↔ ¬ ∃ W : WeightsN 6 4 ℂ, EqSystemN 6 4 W := ⊢ True ↔ ¬∃ W, EqSystemN 6 4 W All goals completed! 🐙

For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem6_no_solution_d5 : answer(sorry) ↔ ¬ ∃ W : WeightsN 6 5 ℂ, EqSystemN 6 5 W := ⊢ True ↔ ¬∃ W, EqSystemN 6 5 W All goals completed! 🐙

For $N = 6$ and $D = 6$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

This follows from eqSystem_no_solution_even_ge4_d_eq_n_explicit.

@[category research solved, AMS 5 14 81, formal_proof using formal_conjectures at "https://github.com/google-deepmind/formal-conjectures/blob/af88acbf9da0f26e3e934743a819e986e02f6875/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L1074"] theorem eqSystem6_no_solution_d6 : answer(True) ↔ ¬ ∃ W : WeightsN 6 6 ℂ, EqSystemN 6 6 W := ⊢ True ↔ ¬∃ W, EqSystemN 6 6 W All goals completed! 🐙

For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem6_no_solution_ge3 : answer(sorry) ↔ ∀ D : Nat, D ≥ 3 → ¬ ∃ W : WeightsN 6 D ℂ, EqSystemN 6 D W := ⊢ True ↔ ∀ D ≥ 3, ¬∃ W, EqSystemN 6 D W All goals completed! 🐙

For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem8_no_solution_d3 : answer(sorry) ↔ ¬ ∃ W : WeightsN 8 3 ℂ, EqSystemN 8 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 8 3 W All goals completed! 🐙

For $N = 8$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

The DeepMind prover agent has found a formal proof of this statement.

@[category research solved, AMS 5 14 81, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/2cc6df2e95835d759caedb15e36b70025b2eae2c/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L853"] theorem eqSystem8_no_solution_d10 : answer(True) ↔ ¬ ∃ W : WeightsN 8 10 ℂ, EqSystemN 8 10 W := ⊢ True ↔ ¬∃ W, EqSystemN 8 10 W All goals completed! 🐙

For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem10_no_solution_d3 : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 3 ℂ, EqSystemN 10 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 3 W All goals completed! 🐙

For $N = 10$ and $D = 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem10_no_solution_d4 : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 4 ℂ, EqSystemN 10 4 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 4 W All goals completed! 🐙

For $N = 10$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem10_no_solution_d5 : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 5 ℂ, EqSystemN 10 5 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 5 W All goals completed! 🐙

For $N = 10$ and $D = 6$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem10_no_solution_d6 : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 6 ℂ, EqSystemN 10 6 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 6 W All goals completed! 🐙

For $N = 10$ and $D = 7$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem10_no_solution_d7 : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 7 ℂ, EqSystemN 10 7 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 7 W All goals completed! 🐙

For $N = 10$ and $D = 8$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem10_no_solution_d8 : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 8 ℂ, EqSystemN 10 8 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 8 W All goals completed! 🐙

For $N = 10$ and $D = 9$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem10_no_solution_d9 : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 9 ℂ, EqSystemN 10 9 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 9 W All goals completed! 🐙

For $N = 10$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

This follows from the $D = N$ case, see eqSystem_no_solution_even_ge4_d_eq_n_explicit.

@[category research solved, AMS 5 14 81, formal_proof using formal_conjectures at "https://github.com/google-deepmind/formal-conjectures/blob/af88acbf9da0f26e3e934743a819e986e02f6875/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L1167"] theorem eqSystem10_no_solution_d10 : answer(True) ↔ ¬ ∃ W : WeightsN 10 10 ℂ, EqSystemN 10 10 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 10 W All goals completed! 🐙

For $N = 12$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem12_no_solution_d3 : answer(sorry) ↔ ¬ ∃ W : WeightsN 12 3 ℂ, EqSystemN 12 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 12 3 W All goals completed! 🐙

For $N = 14$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem14_no_solution_d3 : answer(sorry) ↔ ¬ ∃ W : WeightsN 14 3 ℂ, EqSystemN 14 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 14 3 W All goals completed! 🐙

For $N = 16$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem16_no_solution_d3 : answer(sorry) ↔ ¬ ∃ W : WeightsN 16 3 ℂ, EqSystemN 16 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 16 3 W All goals completed! 🐙

For all even $N \geq 6$ and $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

@[category research open, AMS 5 14 81] theorem eqSystem_no_solution_ge6_ge3 : answer(sorry) ↔ ∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 → ¬ ∃ W : WeightsN N D ℂ, EqSystemN N D W := ⊢ True ↔ ∀ (N D : ℕ), N ≥ 6 → Even N → D ≥ 3 → ¬∃ W, EqSystemN N D W All goals completed! 🐙

For $N = 4$ and all $D \geq 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

This follows from the solution of the complex version of the problem (see eqSystem4_no_solution_ge4)

@[category research solved, AMS 5 14 81, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/4854c7233c58a7dce45fdd58b1826abf2c9c1a0f/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L738"] theorem eqSystem4_no_solution_ge4_real : answer(True) ↔ ∀ D : Nat, D ≥ 4 → ¬ ∃ W : WeightsN 4 D ℝ, EqSystemN 4 D W := ⊢ True ↔ ∀ D ≥ 4, ¬∃ W, EqSystemN 4 D W All goals completed! 🐙

For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

@[category research open, AMS 5 14 81] theorem eqSystem6_no_solution_d3_real : answer(sorry) ↔ ¬ ∃ W : WeightsN 6 3 ℝ, EqSystemN 6 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 6 3 W All goals completed! 🐙

For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

@[category research open, AMS 5 14 81] theorem eqSystem6_no_solution_d5_real : answer(sorry) ↔ ¬ ∃ W : WeightsN 6 5 ℝ, EqSystemN 6 5 W := ⊢ True ↔ ¬∃ W, EqSystemN 6 5 W All goals completed! 🐙

For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

@[category research open, AMS 5 14 81] theorem eqSystem6_no_solution_ge3_real : answer(sorry) ↔ ∀ D : Nat, D ≥ 3 → ¬ ∃ W : WeightsN 6 D ℝ, EqSystemN 6 D W := ⊢ True ↔ ∀ D ≥ 3, ¬∃ W, EqSystemN 6 D W All goals completed! 🐙

For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

@[category research open, AMS 5 14 81] theorem eqSystem8_no_solution_d3_real : answer(sorry) ↔ ¬ ∃ W : WeightsN 8 3 ℝ, EqSystemN 8 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 8 3 W All goals completed! 🐙

For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

@[category research open, AMS 5 14 81] theorem eqSystem10_no_solution_d3_real : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 3 ℝ, EqSystemN 10 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 3 W All goals completed! 🐙

For all even $N \geq 6$ and $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

@[category research open, AMS 5 14 81] theorem eqSystem_no_solution_ge6_ge3_real : answer(sorry) ↔ ∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 → ¬ ∃ W : WeightsN N D ℝ, EqSystemN N D W := ⊢ True ↔ ∀ (N D : ℕ), N ≥ 6 → Even N → D ≥ 3 → ¬∃ W, EqSystemN N D W All goals completed! 🐙

For $N = 4$ and all $D \geq 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?

This follows from the solution of the complex version of the problem (see eqSystem4_no_solution_ge4).

@[category research solved, AMS 5 14 81, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/4854c7233c58a7dce45fdd58b1826abf2c9c1a0f/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L836"] theorem eqSystem4_no_solution_ge4_int : answer(True) ↔ ∀ D : Nat, D ≥ 4 → ¬ ∃ W : WeightsN 4 D ℤ, EqSystemN 4 D W := ⊢ True ↔ ∀ D ≥ 4, ¬∃ W, EqSystemN 4 D W All goals completed! 🐙

For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?

@[category research open, AMS 5 14 81] theorem eqSystem6_no_solution_d3_int : answer(sorry) ↔ ¬ ∃ W : WeightsN 6 3 ℤ, EqSystemN 6 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 6 3 W All goals completed! 🐙

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] theorem eqSystem6_no_solution_d5_int : answer(sorry) ↔ ¬ ∃ W : WeightsN 6 5 ℤ, EqSystemN 6 5 W := ⊢ True ↔ ¬∃ W, EqSystemN 6 5 W All goals completed! 🐙

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] theorem eqSystem6_no_solution_ge3_int : answer(sorry) ↔ ∀ D : Nat, D ≥ 3 → ¬ ∃ W : WeightsN 6 D ℤ, EqSystemN 6 D W := ⊢ True ↔ ∀ D ≥ 3, ¬∃ W, EqSystemN 6 D W All goals completed! 🐙

For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?

@[category research open, AMS 5 14 81] theorem eqSystem8_no_solution_d3_int : answer(sorry) ↔ ¬ ∃ W : WeightsN 8 3 ℤ, EqSystemN 8 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 8 3 W All goals completed! 🐙

For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?

@[category research open, AMS 5 14 81] theorem eqSystem10_no_solution_d3_int : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 3 ℤ, EqSystemN 10 3 W := ⊢ True ↔ ¬∃ W, EqSystemN 10 3 W All goals completed! 🐙

For all even $N \geq 6$ and $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] theorem eqSystem_no_solution_ge6_ge3_int : answer(sorry) ↔ ∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 → ¬ ∃ W : WeightsN N D ℤ, EqSystemN N D W := ⊢ True ↔ ∀ (N D : ℕ), N ≥ 6 → Even N → D ≥ 3 → ¬∃ W, EqSystemN N D W All goals completed! 🐙

For $N = 4$ and all $D \geq 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$ with weights in ${-1, 0, 1}$?

This follows from the complex version, see eqSystem4_no_solution_ge4.

@[category research solved, AMS 5 14 81, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/4854c7233c58a7dce45fdd58b1826abf2c9c1a0f/FormalConjectures/Paper/MonochromaticQuantumGraph.lean#L936"] theorem eqSystem4_no_solution_ge4_trinary_int : answer(True) ↔ ∀ D : Nat, D ≥ 4 → ¬ ∃ W : WeightsN 4 D ℤ, (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 4 D W := ⊢ True ↔ ∀ D ≥ 4, ¬∃ W, (∀ (e : EdgeN 4 D), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 4 D W All goals completed! 🐙

For $N = 6$ and $D = 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] theorem eqSystem6_no_solution_d3_trinary_int : answer(sorry) ↔ ¬ ∃ W : WeightsN 6 3 ℤ, (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 6 3 W := ⊢ True ↔ ¬∃ W, (∀ (e : EdgeN 6 3), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 6 3 W All goals completed! 🐙

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] theorem eqSystem6_no_solution_d5_trinary_int : answer(sorry) ↔ ¬ ∃ W : WeightsN 6 5 ℤ, (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 6 5 W := ⊢ True ↔ ¬∃ W, (∀ (e : EdgeN 6 5), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 6 5 W All goals completed! 🐙

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] theorem eqSystem6_no_solution_ge3_trinary_int : answer(sorry) ↔ ∀ D : Nat, D ≥ 3 → ¬ ∃ W : WeightsN 6 D ℤ, (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 6 D W := ⊢ True ↔ ∀ D ≥ 3, ¬∃ W, (∀ (e : EdgeN 6 D), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 6 D W All goals completed! 🐙

For $N = 8$ and $D = 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] theorem eqSystem8_no_solution_d3_trinary_int : answer(sorry) ↔ ¬ ∃ W : WeightsN 8 3 ℤ, (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 8 3 W := ⊢ True ↔ ¬∃ W, (∀ (e : EdgeN 8 3), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 8 3 W All goals completed! 🐙

For $N = 10$ and $D = 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] theorem eqSystem10_no_solution_d3_trinary_int : answer(sorry) ↔ ¬ ∃ W : WeightsN 10 3 ℤ, (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 10 3 W := ⊢ True ↔ ¬∃ W, (∀ (e : EdgeN 10 3), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 10 3 W All goals completed! 🐙

For all even $N \geq 6$ and $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] theorem eqSystem_no_solution_ge6_ge3_trinary_int : answer(sorry) ↔ ∀ N D : Nat, N ≥ 6 → Even N → D ≥ 3 → ¬ ∃ W : WeightsN N D ℤ, (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN N D W := ⊢ True ↔ ∀ (N D : ℕ), N ≥ 6 → Even N → D ≥ 3 → ¬∃ W, (∀ (e : EdgeN N D), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN N D W All goals completed! 🐙end MonochromaticQuantumGraph