MonochromaticQuantumGraph.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

68 declarations, 45 contain sorry, 0 declared as axioms

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.
[Ki26] A solver-free Lean 4 proof of the sharp bound $D \le N - 2$ for monochromatic quantum graph equation systems over integral domains, commit 6c534038.
[Ki26b] A solver-free Lean 4 proof that the monochromatic quantum graph equation system has no solution for $N = 10$ and $D = 8$ over integral domains, commit a9309005.

Imports (1)

FormalConjecturesUtil

Imported by 2 files

abbrev MonochromaticQuantumGraph.V Vertices of $K_N$ line 92 source
Source documentation
Vertices of $K_N$.

no axioms what this means
Statement uses: Nat
Proof uses: Fin
```
abbrev V (N : Nat) := Fin N
```
structure MonochromaticQuantumGraph.EdgeN Edge label for $K_N$ with endpoint indices in Fin D line 99 source
Source documentation
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.

no axioms what this means
Statement uses: Nat
```
structure EdgeN (N D : Nat) where
…
```
abbrev MonochromaticQuantumGraph.WeightsN Weights on edges line 107 source
Source documentation
Weights on edges.

no axioms what this means
Statement uses: Nat
Proof uses: MonochromaticQuantumGraph.EdgeN
```
abbrev WeightsN (N D : Nat) (α : Type) := EdgeN N D → α
```
Mentions: MonochromaticQuantumGraph.EdgeN
def MonochromaticQuantumGraph.mkEdge Helper: build an EdgeN from endpoints and endpoint indices line 110 source
Source documentation
Helper: build an EdgeN from endpoints and endpoint indices.

no axioms what this means
Statement uses: Nat, MonochromaticQuantumGraph.V, Fin, MonochromaticQuantumGraph.EdgeN
Proof uses: MonochromaticQuantumGraph.EdgeN.mk
```
def mkEdge {N D : Nat} (u v : V N) (i j : Fin D) : EdgeN N D :=
…
```
Mentions: MonochromaticQuantumGraph.V, MonochromaticQuantumGraph.EdgeN

def MonochromaticQuantumGraph.vertices Ordered vertex list $[0, 1, \ldots, N-1]$ line 114 source

Source documentation

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

standard axioms: propext what this means

Statement uses: Nat, List, MonochromaticQuantumGraph.V

2 instances, coercions and auxiliary constants left out.

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

/-
## `allEqual`: "all indices are equal"

We package the property "all indices `ι v` are equal" as a chain condition along a vertex list.

Concretely, `allEqualList ι L` means that the relation `ι v = ι w` holds between adjacent elements
of `L`. We implement this with `List.IsChain`, which is convenient for later reasoning and provides

Mentions: MonochromaticQuantumGraph.V, MonochromaticQuantumGraph.allEqual, MonochromaticQuantumGraph.allEqualList

def MonochromaticQuantumGraph.allEqualList Chain-equality along a list of vertices line 130 source
Source documentation
Chain-equality along a list of vertices.

no axioms what this means
Statement uses: Nat, MonochromaticQuantumGraph.V, Fin, List
Proof uses: List.IsChain, Eq
```
def allEqualList {N D : Nat} (ι : V N → Fin D) (L : List (V N)) : Prop :=
…
```
Mentions: MonochromaticQuantumGraph.V
def MonochromaticQuantumGraph.allEqual All indices equal on Fin N (using the canonical ordered vertex list) line 134 source
Source documentation
All indices equal on Fin N (using the canonical ordered vertex list).

standard axioms: propext what this means
Statement uses: Nat, MonochromaticQuantumGraph.V, Fin
Proof uses: MonochromaticQuantumGraph.allEqualList, MonochromaticQuantumGraph.vertices

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def allEqual {N D : Nat} (ι : V N → Fin D) : Prop :=
…
```
Mentions: MonochromaticQuantumGraph.V
instance MonochromaticQuantumGraph.(instance at line 138) line 138 source
Source documentation
Instance: allEqualList ι L is decidable.
```
instance {N D : Nat} (ι : V N → Fin D) (L : List (V N)) :
    Decidable (allEqualList ι L) := by
…
```
Mentions: MonochromaticQuantumGraph.V, MonochromaticQuantumGraph.allEqualList
instance MonochromaticQuantumGraph.(instance at line 145) line 145 source
Source documentation
Instance: allEqual ι is decidable.
```
instance {N D : Nat} (ι : V N → Fin D) : Decidable (allEqual ι) := by
…
```
Mentions: MonochromaticQuantumGraph.V, MonochromaticQuantumGraph.allEqual
def MonochromaticQuantumGraph.pmSumListAux Auxiliary perfect-matching sum on a vertex list, using a fuel parameter n for termination line 175 source
Source documentation
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.

standard axioms: propext what this means
Statement uses: Semiring, Nat, MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.V, Fin, List
2 instances, coercions and auxiliary constants left out.
```
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
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.V, MonochromaticQuantumGraph.mkEdge
def MonochromaticQuantumGraph.pmSumList Perfect-matching sum on a list: run pmSumListAux with fuel = L.length line 189 source
Source documentation
Perfect-matching sum on a list: run pmSumListAux with fuel = L.length.

standard axioms: propext what this means
Statement uses: Semiring, Nat, MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.V, Fin, List
Proof uses: MonochromaticQuantumGraph.pmSumListAux, List.length
```
def pmSumList {α : Type} [Semiring α] {N D : Nat}
    (W : WeightsN N D α) (ι : V N → Fin D) (L : List (V N)) : α :=
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.V
def MonochromaticQuantumGraph.pmSumN The perfect-matching sum for $K_N$: use the canonical ordered vertex list vertices N line 194 source
Source documentation
The perfect-matching sum for $K_N$: use the canonical ordered vertex list vertices N.

standard axioms: propext what this means
Statement uses: Semiring, Nat, MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.V, Fin
Proof uses: MonochromaticQuantumGraph.pmSumList, MonochromaticQuantumGraph.vertices
```
def pmSumN {α : Type} [Semiring α] (N D : Nat)
    (W : WeightsN N D α) (ι : V N → Fin D) : α :=
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.V
def MonochromaticQuantumGraph.EqSystemN The monochromatic quantum graph equation system for $K_N$ line 202 source
Source documentation
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.

standard axioms: propext what this means
Statement uses: Semiring, Nat, MonochromaticQuantumGraph.WeightsN
Proof uses: MonochromaticQuantumGraph.V, Fin, Eq, MonochromaticQuantumGraph.pmSumN, ite, MonochromaticQuantumGraph.allEqual, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
```
def EqSystemN {α : Type} [Semiring α] (N D : Nat) (W : WeightsN N D α) : Prop :=
…
```
Mentions: MonochromaticQuantumGraph.WeightsN
instance MonochromaticQuantumGraph.instDecidableEqSystemN Instance: EqSystemN N D W is decidable when α has decidable equality line 216 source
Source documentation
Instance: EqSystemN N D W is decidable when α has decidable equality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Semiring, DecidableEq, MonochromaticQuantumGraph.WeightsN, Decidable, MonochromaticQuantumGraph.EqSystemN
Proof uses: MonochromaticQuantumGraph.V, Fin, Eq, MonochromaticQuantumGraph.pmSumN, ite, MonochromaticQuantumGraph.allEqual, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.
```
instance instDecidableEqSystemN {N D : Nat} {α : Type} [Semiring α] [DecidableEq α]
    (W : WeightsN N D α) : Decidable (EqSystemN N D W) :=
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
def MonochromaticQuantumGraph.Witness4_d2 line 224 source
standard axioms: propext what this means
Statement uses: Semiring, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat
Proof uses: MonochromaticQuantumGraph.EdgeN, ite, Eq, MonochromaticQuantumGraph.mkEdge, MonochromaticQuantumGraph.V, Fin
14 instances, coercions and auxiliary constants left out.
theorem MonochromaticQuantumGraph.eqSystem4_d2_nat Sanity check over ℕ using native_decide line 234 source
Source documentation
Sanity check over ℕ using native_decide.
```
private theorem eqSystem4_d2_nat :
    EqSystemN 4 2 (Witness4_d2 (α := ℕ)) := by
…
```
Mentions: MonochromaticQuantumGraph.EqSystemN, MonochromaticQuantumGraph.Witness4_d2
theorem MonochromaticQuantumGraph.eqSystem4_has_solution_d2 line 239 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Semiring, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, MonochromaticQuantumGraph.EqSystemN
Proof uses: Exists.intro, MonochromaticQuantumGraph.Witness4_d2, MonochromaticQuantumGraph.V, Fin, Eq, MonochromaticQuantumGraph.pmSumN, Matrix.vecCons, Matrix.vecEmpty, ite, MonochromaticQuantumGraph.allEqual, Nat.succ, Eq.mpr, HAdd.hAdd, And, id, congr, congrArg, Eq.trans, MonochromaticQuantumGraph.pmSumListAux, List.length and 66 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
def MonochromaticQuantumGraph.Witness4_d3 line 261 source
standard axioms: propext what this means
Statement uses: Semiring, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat
Proof uses: MonochromaticQuantumGraph.EdgeN, ite, Eq, MonochromaticQuantumGraph.mkEdge, MonochromaticQuantumGraph.V, Fin
14 instances, coercions and auxiliary constants left out.
theorem MonochromaticQuantumGraph.eqSystem4_d3_nat Sanity check over ℕ using native_decide line 273 source
Source documentation
Sanity check over ℕ using native_decide.
```
private theorem eqSystem4_d3_nat :
    EqSystemN 4 3 (Witness4_d3 (α := ℕ)) := by
…
```
Mentions: MonochromaticQuantumGraph.EqSystemN, MonochromaticQuantumGraph.Witness4_d3
theorem MonochromaticQuantumGraph.eqSystem4_has_solution_d3 line 278 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Semiring, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, MonochromaticQuantumGraph.EqSystemN
Proof uses: Exists.intro, MonochromaticQuantumGraph.Witness4_d3, MonochromaticQuantumGraph.V, Fin, Eq, MonochromaticQuantumGraph.pmSumN, Matrix.vecCons, Matrix.vecEmpty, ite, MonochromaticQuantumGraph.allEqual, Nat.succ, Eq.mpr, HAdd.hAdd, And, id, congr, congrArg, Eq.trans, MonochromaticQuantumGraph.pmSumListAux, List.length and 66 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
def MonochromaticQuantumGraph.Witness6_d2 line 300 source
standard axioms: propext what this means
Statement uses: Semiring, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat
Proof uses: MonochromaticQuantumGraph.EdgeN, ite, Eq, MonochromaticQuantumGraph.mkEdge, MonochromaticQuantumGraph.V, Fin
14 instances, coercions and auxiliary constants left out.
theorem MonochromaticQuantumGraph.eqSystem6_d2_nat Sanity check over ℕ using native_decide line 312 source
Source documentation
Sanity check over ℕ using native_decide.
```
private theorem eqSystem6_d2_nat :
    EqSystemN 6 2 (Witness6_d2 (α := ℕ)) := by
…
```
Mentions: MonochromaticQuantumGraph.EqSystemN, MonochromaticQuantumGraph.Witness6_d2
theorem MonochromaticQuantumGraph.eqSystem6_has_solution_d2 line 317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Semiring, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, MonochromaticQuantumGraph.EqSystemN
Proof uses: Exists.intro, MonochromaticQuantumGraph.Witness6_d2, MonochromaticQuantumGraph.V, Fin, Eq, MonochromaticQuantumGraph.pmSumN, Matrix.vecCons, Matrix.vecEmpty, ite, MonochromaticQuantumGraph.allEqual, Nat.succ, Eq.mpr, HAdd.hAdd, And, id, congr, congrArg, Eq.trans, MonochromaticQuantumGraph.pmSumListAux, List.length and 66 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem4_no_solution_nnreal_ge4 Bogdanov: for $N = 4$ and all $D \geq 4$, no solution exists over $\mathbb{R}_{\geq 0}$ sorry line 346 source
Source documentation
Bogdanov: for $N = 4$ and all $D \geq 4$, no solution exists over $\mathbb{R}_{\geq 0}$.

depends on sorry what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Not, Exists, MonochromaticQuantumGraph.WeightsN, NNReal, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem4_no_solution_nnreal_ge4 :
    ∀ D : Nat, D ≥ 4 →
      ¬ ∃ W : WeightsN 4 D ℝ≥0, EqSystemN 4 D W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem_no_solution_nnreal_even_ge6_ge3 Bogdanov: for all even $N \geq 6$ and $D \geq 3$, no solution exists over $\mathbb{R}_{\geq 0}$ sorry line 353 source
Source documentation
Bogdanov: for all even $N \geq 6$ and $D \geq 3$, no solution exists over $\mathbb{R}_{\geq 0}$.

depends on sorry what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Even, Not, Exists, MonochromaticQuantumGraph.WeightsN, NNReal, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem_no_solution_even_ge4_d_eq_n_explicit sorry line 382 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Even, Not, Exists, MonochromaticQuantumGraph.WeightsN, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem4_no_solution_d4 sorry line 394 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem4_no_solution_ge4 sorry line 407 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Not, Exists, MonochromaticQuantumGraph.WeightsN, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d3 sorry line 421 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d4 sorry line 432 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d5 sorry line 444 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d6 sorry line 456 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3 For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 464 source
Source documentation
For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Not, Exists, MonochromaticQuantumGraph.WeightsN, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem6_no_solution_ge3 :
    answer(sorry) ↔
      ∀ D : Nat, D ≥ 3 →
        ¬ ∃ W : WeightsN 6 D ℂ, EqSystemN 6 D W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d3 For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 473 source
Source documentation
For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem8_no_solution_d3 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 8 3 ℂ, EqSystemN 8 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d10 sorry line 485 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3 For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 493 source
Source documentation
For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem10_no_solution_d3 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 10 3 ℂ, EqSystemN 10 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d4 For $N = 10$ and $D = 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 501 source
Source documentation
For $N = 10$ and $D = 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem10_no_solution_d4 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 10 4 ℂ, EqSystemN 10 4 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d5 For $N = 10$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 509 source
Source documentation
For $N = 10$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem10_no_solution_d5 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 10 5 ℂ, EqSystemN 10 5 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d6 For $N = 10$ and $D = 6$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 517 source
Source documentation
For $N = 10$ and $D = 6$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem10_no_solution_d6 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 10 6 ℂ, EqSystemN 10 6 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d7 For $N = 10$ and $D = 7$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 525 source
Source documentation
For $N = 10$ and $D = 7$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem10_no_solution_d7 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 10 7 ℂ, EqSystemN 10 7 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d8 sorry line 538 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d9 sorry line 549 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d10 sorry line 560 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem12_no_solution_d3 For $N = 12$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 568 source
Source documentation
For $N = 12$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem12_no_solution_d3 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 12 3 ℂ, EqSystemN 12 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem14_no_solution_d3 For $N = 14$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 576 source
Source documentation
For $N = 14$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem14_no_solution_d3 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 14 3 ℂ, EqSystemN 14 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem16_no_solution_d3 For $N = 16$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 584 source
Source documentation
For $N = 16$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem16_no_solution_d3 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 16 3 ℂ, EqSystemN 16 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3 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}$? sorry line 594 source
Source documentation
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}$?

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Even, Not, Exists, MonochromaticQuantumGraph.WeightsN, Complex, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_real sorry line 611 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Not, Exists, MonochromaticQuantumGraph.WeightsN, Real, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d3_real For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$? sorry line 620 source
Source documentation
For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Real, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem6_no_solution_d3_real :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 6 3 ℝ, EqSystemN 6 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d5_real sorry line 631 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Real, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_real For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$? sorry line 639 source
Source documentation
For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Not, Exists, MonochromaticQuantumGraph.WeightsN, Real, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem6_no_solution_ge3_real :
    answer(sorry) ↔
      ∀ D : Nat, D ≥ 3 →
        ¬ ∃ W : WeightsN 6 D ℝ, EqSystemN 6 D W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d3_real For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$? sorry line 648 source
Source documentation
For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Real, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem8_no_solution_d3_real :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 8 3 ℝ, EqSystemN 8 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3_real For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$? sorry line 658 source
Source documentation
For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?

depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Real, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eqSystem10_no_solution_d3_real :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 10 3 ℝ, EqSystemN 10 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_real 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}$? sorry line 666 source
Source documentation
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}$?

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Even, Not, Exists, MonochromaticQuantumGraph.WeightsN, Real, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_int sorry line 682 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Not, Exists, MonochromaticQuantumGraph.WeightsN, Int, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d3_int sorry line 693 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Int, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d5_int sorry line 703 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Int, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_int sorry line 713 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Not, Exists, MonochromaticQuantumGraph.WeightsN, Int, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d3_int sorry line 724 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Int, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3_int sorry line 735 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Int, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_int sorry line 745 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Even, Not, Exists, MonochromaticQuantumGraph.WeightsN, Int, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_trinary_int sorry line 761 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Not, Exists, MonochromaticQuantumGraph.WeightsN, Int, And, MonochromaticQuantumGraph.EdgeN, Or, Eq, Neg.neg, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d3_trinary_int sorry line 774 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Int, And, MonochromaticQuantumGraph.EdgeN, Or, Eq, Neg.neg, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d5_trinary_int sorry line 786 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Int, And, MonochromaticQuantumGraph.EdgeN, Or, Eq, Neg.neg, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_trinary_int sorry line 798 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Not, Exists, MonochromaticQuantumGraph.WeightsN, Int, And, MonochromaticQuantumGraph.EdgeN, Or, Eq, Neg.neg, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d3_trinary_int sorry line 811 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Int, And, MonochromaticQuantumGraph.EdgeN, Or, Eq, Neg.neg, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3_trinary_int sorry line 824 source
depends on sorry what this means
Statement uses: Iff, True, Not, Exists, MonochromaticQuantumGraph.WeightsN, OfNat.ofNat, Nat, Int, And, MonochromaticQuantumGraph.EdgeN, Or, Eq, Neg.neg, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_trinary_int sorry line 836 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Even, Not, Exists, MonochromaticQuantumGraph.WeightsN, Int, And, MonochromaticQuantumGraph.EdgeN, Or, Eq, Neg.neg, MonochromaticQuantumGraph.EqSystemN
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.