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

• [Krenn2017] M. Krenn, X. Gu, A. Zeilinger, "Quantum Experiments and Graphs: Multiparty States as Coherent Superpositions of Perfect Matchings", Physical Review Letters 119(24), 240403 (2017).

• [MO2018] Vertex coloring inherited from perfect matchings (motivated by quantum physics), MathOverflow question 311325.

• [Gu2019] X. Gu, M. Erhard, A. Zeilinger, M. Krenn, "Quantum experiments and graphs II: Quantum interference, computation, and state generation", PNAS 116(10), 4147–4155 (2019).

• [Krenn2019] Questions on the Structure of Perfect Matchings inspired by Quantum Physics by M. Krenn, X. Gu, U. Soltész, Proc. 2nd Croatian Combinatorial Days, 57–70 (2019).

• [Chandran2022] Edge-coloured graphs with only monochromatic perfect matchings and their connection to quantum physics by N. Chandran, S. Gajjala (2022).

• [Chandran2024] Krenn–Gu conjecture for sparse graphs by N. Chandran, S. Gajjala, S. Illickan, M. Krenn, MFCS 2024.

@[reducible, inline]

abbrev MonochromaticQuantumGraph.V (N : ℕ) : Type

Vertices of $K_N$.

Equations

• MonochromaticQuantumGraph.V N = Fin N

structure MonochromaticQuantumGraph.EdgeN (N D : ℕ) : Type

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.

• u : V N
• v : V N
• i : Fin D
• j : Fin D

instance MonochromaticQuantumGraph.instDecidableEqEdgeN {N✝ D✝ : ℕ} : DecidableEq (EdgeN N✝ D✝)

Equations

• MonochromaticQuantumGraph.instDecidableEqEdgeN = MonochromaticQuantumGraph.instDecidableEqEdgeN.decEq

def MonochromaticQuantumGraph.instDecidableEqEdgeN.decEq {N✝ D✝ : ℕ} (x✝ x✝¹ : EdgeN N✝ D✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MonochromaticQuantumGraph.WeightsN (N D : ℕ) (α : Type) : Type

Weights on edges.

Equations

• MonochromaticQuantumGraph.WeightsN N D α = (MonochromaticQuantumGraph.EdgeN N D → α)

def MonochromaticQuantumGraph.mkEdge {N D : ℕ} (u v : V N) (i j : Fin D) : EdgeN N D

Helper: build an EdgeN from endpoints and endpoint indices.

Equations

• MonochromaticQuantumGraph.mkEdge u v i j = { u := u, v := v, i := i, j := j }

def MonochromaticQuantumGraph.vertices (N : ℕ) : List (V N)

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

Equations

• MonochromaticQuantumGraph.vertices 0 = []
• MonochromaticQuantumGraph.vertices N.succ = 0 :: List.map Fin.succ (MonochromaticQuantumGraph.vertices N)

def MonochromaticQuantumGraph.allEqualList {N D : ℕ} (ι : V N → Fin D) (L : List (V N)) : Prop

Chain-equality along a list of vertices.

Equations

• MonochromaticQuantumGraph.allEqualList ι L = List.IsChain (fun (v w : MonochromaticQuantumGraph.V N) => ι v = ι w) L

def MonochromaticQuantumGraph.allEqual {N D : ℕ} (ι : V N → Fin D) : Prop

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

Equations

• MonochromaticQuantumGraph.allEqual ι = MonochromaticQuantumGraph.allEqualList ι (MonochromaticQuantumGraph.vertices N)

instance MonochromaticQuantumGraph.instDecidableAllEqualList {N D : ℕ} (ι : V N → Fin D) (L : List (V N)) : Decidable (allEqualList ι L)

Instance: allEqualList ι L is decidable.

Equations

• MonochromaticQuantumGraph.instDecidableAllEqualList ι L = id inferInstance

instance MonochromaticQuantumGraph.instDecidableAllEqual {N D : ℕ} (ι : V N → Fin D) : Decidable (allEqual ι)

Instance: allEqual ι is decidable.

Equations

• MonochromaticQuantumGraph.instDecidableAllEqual ι = id inferInstance

def MonochromaticQuantumGraph.pmSumListAux {α : Type} [Semiring α] {N D : ℕ} (W : WeightsN N D α) (ι : V N → Fin D) : ℕ → List (V N) → α

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.

Equations

• One or more equations did not get rendered due to their size.
• MonochromaticQuantumGraph.pmSumListAux W ι 0 x✝ = 1
• MonochromaticQuantumGraph.pmSumListAux W ι 1 x✝ = 0
• MonochromaticQuantumGraph.pmSumListAux W ι n.succ.succ [] = 1
• MonochromaticQuantumGraph.pmSumListAux W ι n.succ.succ [head] = 0

def MonochromaticQuantumGraph.pmSumList {α : Type} [Semiring α] {N D : ℕ} (W : WeightsN N D α) (ι : V N → Fin D) (L : List (V N)) : α

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

Equations

• MonochromaticQuantumGraph.pmSumList W ι L = MonochromaticQuantumGraph.pmSumListAux W ι L.length L

def MonochromaticQuantumGraph.pmSumN {α : Type} [Semiring α] (N D : ℕ) (W : WeightsN N D α) (ι : V N → Fin D) : α

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

Equations

• MonochromaticQuantumGraph.pmSumN N D W ι = MonochromaticQuantumGraph.pmSumList W ι (MonochromaticQuantumGraph.vertices N)

def MonochromaticQuantumGraph.EqSystemN {α : Type} [Semiring α] (N D : ℕ) (W : WeightsN N D α) : Prop

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.

Equations

• MonochromaticQuantumGraph.EqSystemN N D W = ∀ (ι : MonochromaticQuantumGraph.V N → Fin D), MonochromaticQuantumGraph.pmSumN N D W ι = if MonochromaticQuantumGraph.allEqual ι then 1 else 0

def MonochromaticQuantumGraph.Witness4_d2 {α : Type} [Semiring α] : WeightsN 4 2 α

Equations

• One or more equations did not get rendered due to their size.

theorem MonochromaticQuantumGraph.eqSystem4_has_solution_d2 {α : Type} [Semiring α] : ∃ (W : WeightsN 4 2 α), EqSystemN 4 2 W

def MonochromaticQuantumGraph.Witness4_d3 : WeightsN 4 3 ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem MonochromaticQuantumGraph.eqSystem4_has_solution_d3 : ∃ (W : WeightsN 4 3 ℂ), EqSystemN 4 3 W

def MonochromaticQuantumGraph.Witness6_d2 {α : Type} [Semiring α] : WeightsN 6 2 α

Equations

• One or more equations did not get rendered due to their size.

theorem MonochromaticQuantumGraph.eqSystem6_has_solution_d2 {α : Type} [Semiring α] : ∃ (W : WeightsN 6 2 α), EqSystemN 6 2 W

theorem MonochromaticQuantumGraph.eqSystem4_no_solution_nnreal_ge4 (D : ℕ) : D ≥ 4 → ¬∃ (W : WeightsN 4 D NNReal), EqSystemN 4 D W

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

theorem MonochromaticQuantumGraph.eqSystem_no_solution_nnreal_even_ge6_ge3 (N D : ℕ) : N ≥ 6 → Even N → D ≥ 3 → ¬∃ (W : WeightsN N D NNReal), EqSystemN N D W

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

theorem MonochromaticQuantumGraph.eqSystem4_no_solution_d4 : True ↔ ¬∃ (W : WeightsN 4 4 ℂ), EqSystemN 4 4 W

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

theorem MonochromaticQuantumGraph.eqSystem4_no_solution_ge4 : True ↔ ∀ D ≥ 4, ¬∃ (W : WeightsN 4 D ℂ), EqSystemN 4 D W

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

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d3 : True ↔ ¬∃ (W : WeightsN 6 3 ℂ), EqSystemN 6 3 W

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

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d4 : True ↔ ¬∃ (W : WeightsN 6 4 ℂ), EqSystemN 6 4 W

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

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d5 : True ↔ ¬∃ (W : WeightsN 6 5 ℂ), EqSystemN 6 5 W

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

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d6 : True ↔ ¬∃ (W : WeightsN 6 6 ℂ), EqSystemN 6 6 W

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

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3 : True ↔ ∀ D ≥ 3, ¬∃ (W : WeightsN 6 D ℂ), EqSystemN 6 D W

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

theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d3 : True ↔ ¬∃ (W : WeightsN 8 3 ℂ), EqSystemN 8 3 W

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

theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d10 : True ↔ ¬∃ (W : WeightsN 8 10 ℂ), EqSystemN 8 10 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3 : True ↔ ¬∃ (W : WeightsN 10 3 ℂ), EqSystemN 10 3 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d4 : True ↔ ¬∃ (W : WeightsN 10 4 ℂ), EqSystemN 10 4 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d5 : True ↔ ¬∃ (W : WeightsN 10 5 ℂ), EqSystemN 10 5 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d6 : True ↔ ¬∃ (W : WeightsN 10 6 ℂ), EqSystemN 10 6 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d7 : True ↔ ¬∃ (W : WeightsN 10 7 ℂ), EqSystemN 10 7 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d8 : True ↔ ¬∃ (W : WeightsN 10 8 ℂ), EqSystemN 10 8 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d9 : True ↔ ¬∃ (W : WeightsN 10 9 ℂ), EqSystemN 10 9 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d10 : True ↔ ¬∃ (W : WeightsN 10 10 ℂ), EqSystemN 10 10 W

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

theorem MonochromaticQuantumGraph.eqSystem12_no_solution_d3 : True ↔ ¬∃ (W : WeightsN 12 3 ℂ), EqSystemN 12 3 W

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

theorem MonochromaticQuantumGraph.eqSystem14_no_solution_d3 : True ↔ ¬∃ (W : WeightsN 14 3 ℂ), EqSystemN 14 3 W

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

theorem MonochromaticQuantumGraph.eqSystem16_no_solution_d3 : True ↔ ¬∃ (W : WeightsN 16 3 ℂ), EqSystemN 16 3 W

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

theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3 : True ↔ ∀ (N D : ℕ), N ≥ 6 → Even N → D ≥ 3 → ¬∃ (W : WeightsN N D ℂ), EqSystemN N D W

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}$?

theorem MonochromaticQuantumGraph.eqSystem4_no_solution_d4_real : True ↔ ¬∃ (W : WeightsN 4 4 ℝ), EqSystemN 4 4 W

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

theorem MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_real : True ↔ ∀ D ≥ 4, ¬∃ (W : WeightsN 4 D ℝ), EqSystemN 4 D W

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

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d3_real : True ↔ ¬∃ (W : WeightsN 6 3 ℝ), EqSystemN 6 3 W

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

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_real : True ↔ ∀ D ≥ 3, ¬∃ (W : WeightsN 6 D ℝ), EqSystemN 6 D W

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

theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d3_real : True ↔ ¬∃ (W : WeightsN 8 3 ℝ), EqSystemN 8 3 W

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

theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d10_real : True ↔ ¬∃ (W : WeightsN 8 10 ℝ), EqSystemN 8 10 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3_real : True ↔ ¬∃ (W : WeightsN 10 3 ℝ), EqSystemN 10 3 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d10_real : True ↔ ¬∃ (W : WeightsN 10 10 ℝ), EqSystemN 10 10 W

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

theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_real : True ↔ ∀ (N D : ℕ), N ≥ 6 → Even N → D ≥ 3 → ¬∃ (W : WeightsN N D ℝ), EqSystemN N D W

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}$?

theorem MonochromaticQuantumGraph.eqSystem4_no_solution_d4_int : True ↔ ¬∃ (W : WeightsN 4 4 ℤ), EqSystemN 4 4 W

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

theorem MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_int : True ↔ ∀ D ≥ 4, ¬∃ (W : WeightsN 4 D ℤ), EqSystemN 4 D W

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

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d3_int : True ↔ ¬∃ (W : WeightsN 6 3 ℤ), EqSystemN 6 3 W

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

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_int : True ↔ ∀ D ≥ 3, ¬∃ (W : WeightsN 6 D ℤ), EqSystemN 6 D W

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

theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d3_int : True ↔ ¬∃ (W : WeightsN 8 3 ℤ), EqSystemN 8 3 W

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

theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d10_int : True ↔ ¬∃ (W : WeightsN 8 10 ℤ), EqSystemN 8 10 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3_int : True ↔ ¬∃ (W : WeightsN 10 3 ℤ), EqSystemN 10 3 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d10_int : True ↔ ¬∃ (W : WeightsN 10 10 ℤ), EqSystemN 10 10 W

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

theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_int : True ↔ ∀ (N D : ℕ), N ≥ 6 → Even N → D ≥ 3 → ¬∃ (W : WeightsN N D ℤ), EqSystemN N D W

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}$?

theorem MonochromaticQuantumGraph.eqSystem4_no_solution_d4_trinary_int : True ↔ ¬∃ (W : WeightsN 4 4 ℤ), (∀ (e : EdgeN 4 4), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 4 4 W

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

theorem MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_trinary_int : True ↔ ∀ D ≥ 4, ¬∃ (W : WeightsN 4 D ℤ), (∀ (e : EdgeN 4 D), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 4 D W

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\}$?

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d3_trinary_int : True ↔ ¬∃ (W : WeightsN 6 3 ℤ), (∀ (e : EdgeN 6 3), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 6 3 W

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\}$?

theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_trinary_int : True ↔ ∀ D ≥ 3, ¬∃ (W : WeightsN 6 D ℤ), (∀ (e : EdgeN 6 D), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 6 D W

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\}$?

theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d3_trinary_int : True ↔ ¬∃ (W : WeightsN 8 3 ℤ), (∀ (e : EdgeN 8 3), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 8 3 W

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\}$?

theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d10_trinary_int : True ↔ ¬∃ (W : WeightsN 8 10 ℤ), (∀ (e : EdgeN 8 10), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 8 10 W

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

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3_trinary_int : True ↔ ¬∃ (W : WeightsN 10 3 ℤ), (∀ (e : EdgeN 10 3), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 10 3 W

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\}$?

theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d10_trinary_int : True ↔ ¬∃ (W : WeightsN 10 10 ℤ), (∀ (e : EdgeN 10 10), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN 10 10 W

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

theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_trinary_int : True ↔ ∀ (N D : ℕ), N ≥ 6 → Even N → D ≥ 3 → ¬∃ (W : WeightsN N D ℤ), (∀ (e : EdgeN N D), W e = -1 ∨ W e = 0 ∨ W e = 1) ∧ EqSystemN N D W

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\}$?