The exact hull is nonempty precisely at feasible targets

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

proven

Loading review…

The polytope $P_r(G,k)$ is nonempty if and only if $G$ has an independent set of size $k$ . Thus certifying emptiness rules out the target $k$ .

Concept map

2 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

Show types on hover

1	import Lax263307.LinearRelaxation
2
3	/-!
4	---
5	title: The exact hull is nonempty precisely at feasible targets
6	type: theorem
7	---
8	The polytope $P_r(G,k)$ is nonempty if and only if $G$ has an independent
9	set of size $k$ . Thus certifying emptiness rules out the target $k$ .
10
11	# Attribution
12
13	Bonnet–Chang, Section 5.1, equation (20).
14	-/
15
16	namespace Lax263307.HullNonempty
17
18	open LinearRelaxation
19
20	/-- Nonemptiness of the exact hull is equivalent to existence of an independent set. -/
21	axiom hull_nonempty_iff {n : ℕ} (G : SimpleGraph (Fin n)) (k r : ℕ) :
22	(independentSetHull G k r).Nonempty ↔
23	∃ I : Finset (Fin n), G.IsIndepSet (I : Set (Fin n)) ∧ I.card = k
24
25	end Lax263307.HullNonempty
26

Bonnet–Chang, Section 5.1, equation (20).

Builds on

Used by

none

From Mathlib

none

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive