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 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were 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 source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

72 declarations, 49 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.

Imports (1)

FormalConjectures.Util.ProblemImports

abbrev MonochromaticQuantumGraph.V Vertices of $K_N$ line 81 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 88 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 96 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 99 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: u, MonochromaticQuantumGraph.V, MonochromaticQuantumGraph.EdgeN
def MonochromaticQuantumGraph.vertices Ordered vertex list $[0, 1, \ldots, N-1]$ line 103 source
Source documentation
Ordered vertex list $[0, 1, \ldots, N-1]$.

standard axioms: propext what this means
Statement uses: Nat, List, MonochromaticQuantumGraph.V
Proof uses: MonochromaticQuantumGraph.vertices.match_1, Unit, OfNat.ofNat, List.nil, Nat.succ, List.cons, HAdd.hAdd, Fin, List.map, Fin.succ
7 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 119 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 123 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 127) line 127 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 134) line 134 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 164 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
Proof uses: MonochromaticQuantumGraph.pmSumListAux.match_1, OfNat.ofNat, Nat.succ, List.sum, List.map, HMul.hMul, MonochromaticQuantumGraph.mkEdge, List.erase
18 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, u, MonochromaticQuantumGraph.mkEdge
def MonochromaticQuantumGraph.pmSumList Perfect-matching sum on a list: run pmSumListAux with fuel = L.length line 178 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 183 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 191 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
10 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 205 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
14 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 213 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
15 instances, coercions and auxiliary constants left out.
theorem MonochromaticQuantumGraph.eqSystem4_d2_nat Sanity check over ℕ using native_decide line 223 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 228 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, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons and 59 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def MonochromaticQuantumGraph.Witness4_d3 line 249 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
15 instances, coercions and auxiliary constants left out.
theorem MonochromaticQuantumGraph.eqSystem4_d3_nat Sanity check over ℕ using native_decide line 261 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 267 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, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons and 59 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def MonochromaticQuantumGraph.Witness6_d2 line 288 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
15 instances, coercions and auxiliary constants left out.
theorem MonochromaticQuantumGraph.eqSystem6_d2_nat Sanity check over ℕ using native_decide line 300 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 306 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, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons and 59 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 17 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 335 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 342 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 No equal-dimension monochromatic quantum graph for even numbers of parties at least four sorry line 371 source
L4DEL explanation
Our agent resolved multiple conjectures of this form, in particular with N = d ∈ {4, 6, 10}.
— George Tsoukalas et al., AlphaProof Nexus paper (Section 4)
Every term in the emerging quantum superposition corresponds to a perfect matching in the graph.
— Mario Krenn, Xuemei Gu, and Anton Zeilinger, Quantum Experiments and Graphs (2017)
one cannot generate monochromatic quantum graphs with dimensions d equal or larger than the number of vertices of the graph
— Mario Krenn's account of the Nexus quantum-optics results
For every even N ≥ 4, no complex edge-weight family on the complete N-vertex graph with N endpoint colors satisfies the monochromatic quantum-graph equations: every constant vertex coloring should have perfect-matching amplitude 1, while every nonconstant coloring should have amplitude 0. This is the equal-dimension case D = N, not the still broader conjecture for every D ≥ 3 when N ≥ 6.
1. EqSystemN N N W is the exact algebraic interface: it sums products of the selected edge weights over all perfect matchings for each assignment of colors to vertices.
2. In the separately linked proof-bearing Formal Conjectures artifact, the argument constructs product test vectors whose contractions annihilate every contribution incident to a distinguished vertex, forcing the graph-side evaluation to be zero.
3. The same test vectors give a nonzero evaluation of the desired monochromatic right-hand side. Equality of the two evaluations would therefore make a nonzero complex number equal to zero, a contradiction.
4. Trust boundary: this AlphaProof Nexus results wrapper ends in by sorry, so this corpus page must retain a local sorry finding. The linked Formal Conjectures source is a separate artifact and is not silently substituted into this build.
Sources and attribution: Pinned Lean source (0647711a7118), George Tsoukalas et al., AlphaProof Nexus paper (Section 4), Pinned proof-bearing Formal Conjectures artifact, Mario Krenn, Xuemei Gu, and Anton Zeilinger, Quantum Experiments and Graphs (2017), Mario Krenn's account of the Nexus quantum-optics results
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_even_ge4_d_eq_n_explicit :
    answer(True) ↔
      ∀ N : Nat, N ≥ 4 → Even N →
        ¬ ∃ W : WeightsN N N ℂ, EqSystemN N N W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem4_no_solution_d4 sorry line 383 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 396 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 For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 405 source
Source documentation
For $N = 6$ 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 eqSystem6_no_solution_d3 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 6 3 ℂ, EqSystemN 6 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d4 For $N = 6$ and $D = 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 414 source
Source documentation
For $N = 6$ 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 eqSystem6_no_solution_d4 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 6 4 ℂ, EqSystemN 6 4 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d5 For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 423 source
Source documentation
For $N = 6$ 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 eqSystem6_no_solution_d5 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 6 5 ℂ, EqSystemN 6 5 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d6 sorry line 435 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 443 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 452 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 For $N = 8$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 460 source
Source documentation
For $N = 8$ and $D = 10$, 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_d10 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 8 10 ℂ, EqSystemN 8 10 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
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 468 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 476 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 484 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 492 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 500 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 For $N = 10$ and $D = 8$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 508 source
Source documentation
For $N = 10$ and $D = 8$, 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_d8 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 10 8 ℂ, EqSystemN 10 8 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d9 For $N = 10$ and $D = 9$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$? sorry line 516 source
Source documentation
For $N = 10$ and $D = 9$, 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_d9 :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 10 9 ℂ, EqSystemN 10 9 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d10 sorry line 527 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 535 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 543 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 551 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 561 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 578 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 587 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 For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$? sorry line 595 source
Source documentation
For $N = 6$ and $D = 5$, 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_d5_real :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 6 5 ℝ, EqSystemN 6 5 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
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 603 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 612 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.eqSystem8_no_solution_d10_real For $N = 8$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$? sorry line 620 source
Source documentation
For $N = 8$ and $D = 10$, 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_d10_real :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 8 10 ℝ, EqSystemN 8 10 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 628 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 636 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 652 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 For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$? sorry line 661 source
Source documentation
For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?

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 eqSystem6_no_solution_d3_int :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 6 3 ℤ, EqSystemN 6 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d5_int For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$? sorry line 669 source
Source documentation
For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?

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 eqSystem6_no_solution_d5_int :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 6 5 ℤ, EqSystemN 6 5 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_int For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$? sorry line 677 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{Z}$?

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 eqSystem6_no_solution_ge3_int :
    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_int For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$? sorry line 686 source
Source documentation
For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?

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 eqSystem8_no_solution_d3_int :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 8 3 ℤ, EqSystemN 8 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d10_int For $N = 8$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$? sorry line 694 source
Source documentation
For $N = 8$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?

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 eqSystem8_no_solution_d10_int :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 8 10 ℤ, EqSystemN 8 10 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3_int For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$? sorry line 702 source
Source documentation
For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?

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 eqSystem10_no_solution_d3_int :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 10 3 ℤ, EqSystemN 10 3 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_int 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}$? sorry line 710 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{Z}$?

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 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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem4_no_solution_d4_trinary_int 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\}$? sorry line 722 source
Source documentation
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\}$?

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 eqSystem4_no_solution_d4_trinary_int :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 4 4 ℤ,
          (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
            EqSystemN 4 4 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_trinary_int sorry line 733 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 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\}$? sorry line 744 source
Source documentation
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\}$?

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 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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_d5_trinary_int 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\}$? sorry line 754 source
Source documentation
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\}$?

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 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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_trinary_int 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\}$? sorry line 764 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{Z}$ with weights in $\{-1, 0, 1\}$?

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 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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d3_trinary_int 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\}$? sorry line 775 source
Source documentation
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\}$?

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 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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem8_no_solution_d10_trinary_int 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\}$? sorry line 785 source
Source documentation
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\}$?

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 eqSystem8_no_solution_d10_trinary_int :
    answer(sorry) ↔
      ¬ ∃ W : WeightsN 8 10 ℤ,
          (∀ e, W e = (-1 : ℤ) ∨ W e = 0 ∨ W e = 1) ∧
            EqSystemN 8 10 W := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem10_no_solution_d3_trinary_int 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\}$? sorry line 795 source
Source documentation
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\}$?

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 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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN
theorem MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_trinary_int 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\}$? sorry line 805 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{Z}$ with weights in $\{-1, 0, 1\}$?

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.
```
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 := by
…
```
Mentions: MonochromaticQuantumGraph.WeightsN, MonochromaticQuantumGraph.EqSystemN