Descending target search in Solve

Lax263307.TargetSearch · concepts/Lax263307/TargetSearch.lean · lax-263307

proven

Loading review…

Natural Language Statement

Theorem

$Solve$ tries targets in descending order. A failed target $k$ is accompanied by a proof that every independent set has size less than $k$ . A successful target returns an independent set of size at least $\rho k$ . The first successful target is therefore a certified upper bound on the independence number, and the returned set retains the factor $\rho$ of that bound. The zero target provides the terminating empty-set case.

Concept map

2 concepts; 3 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax263307.TargetSearch

⊢Lax263307Proofs.TargetSearch.search_correct

Lean source view on GitHub

Show types on hover

1	import Lax263307.LinearRelaxation
2	import Mathlib.Data.Rat.Defs
3
4	/-!
5	---
6	title: Descending target search in Solve
7	type: theorem
8	---
9	`Solve` tries targets in descending order. A failed target $k$ is accompanied
10	by a proof that every independent set has size less than $k$ . A successful
11	target returns an independent set of size at least $\rho k$ .
12	The first successful target is therefore a certified upper bound on the
13	independence number, and the returned set retains the factor $\rho$ of that
14	bound. The zero target provides the terminating empty-set case.
15
16	# Attribution
17
18	Bonnet–Chang, Algorithm 1 and the last paragraph of the proof of Lemma 14.
19	-/
20
21	namespace Lax263307.TargetSearch
22
23	/-- Try positive targets in decreasing order, falling back to the empty set. -/
24	def search {n : ℕ} (attempt : ℕ → Option (Finset (Fin n))) :
25	ℕ → Finset (Fin n) × ℕ
26	\| 0 => (∅, 0)
27	\| k + 1 => match attempt (k + 1) with
28	\| some I => (I, k + 1)
29	\| none => search attempt k
30
31	/-- The target loop preserves the upper-bound and approximation invariants. -/
32	axiom search_correct {n : ℕ} (G : SimpleGraph (Fin n)) (ρ : ℝ)
33	(attempt : ℕ → Option (Finset (Fin n)))
34	(success : ∀ k, k ≤ n → ∀ I, attempt k = some I →
35	G.IsIndepSet (I : Set (Fin n)) ∧ ρ * k ≤ I.card)
36	(failure : ∀ k, 0 < k → k ≤ n → attempt k = none →
37	∀ J : Finset (Fin n), G.IsIndepSet (J : Set (Fin n)) → J.card < k) :
38	let result := search attempt n
39	G.IsIndepSet (result.1 : Set (Fin n)) ∧
40	(∀ J : Finset (Fin n), G.IsIndepSet (J : Set (Fin n)) → J.card ≤ result.2) ∧
41	result.2 ≤ n ∧ ρ * result.2 ≤ result.1.card
42
43	end Lax263307.TargetSearch
44