A width obstruction from sparse costs and bounded route loads

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

proven

Loading review…

Natural Language Statement

Theorem

Assume vertex costs lie in $[0,1]$ , have total mass at most $k>0$ , and edge cost at most $k^2/p$ . A route distribution with vertex loads at most $\ell x_v/k$ satisfies the sampling budgets for any source graph with $m$ edges when $k\ge8m^2\ell^2$ and $p\ge16m^2\ell^2$ . Consequently, for a source graph of maximum degree $d$ , a monotone class bag bound $W$ forces a discarded-edge count $q$ with $Lq\le4m\ell$ and the pruned source treewidth-plus-one bound.

Concept map

32 concepts; 9 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

- thm✓Lax263307.InducedEmbeddingWidth
- thm✓Lax263307.PathSampling
→
thm✓Lax263307.CostSamplingObstruction
⊢Lax263307Proofs.CostSamplingObstruction.cost_width_obstruction

Lean source view on GitHub

Show types on hover

1	import Lax263307.InducedEmbeddingWidth
2
3	/-!
4	---
5	title: A width obstruction from sparse costs and bounded route loads
6	type: theorem
7	---
8	Assume vertex costs lie in $[0,1]$ , have total mass at most $k>0$ , and
9	edge cost at most $k^2/p$ . A route distribution with vertex loads at most
10	$\ell x_v/k$ satisfies the sampling budgets for any source graph with
11	$m$ edges when $k\ge8m^2\ell^2$ and $p\ge16m^2\ell^2$ .
12	Consequently, for a source graph of maximum degree $d$ , a monotone class
13	bag bound $W$ forces a discarded-edge count $q$ with
14	$Lq\le4m\ell$ and the pruned source treewidth-plus-one bound.
15
16	# Formalization notes
17
18	The class bag bound is still an explicit intermediate hypothesis. This
19	combines the proved probability estimates and sampled width obstruction;
20	it does not yet derive the class bound from separators.
21
22	# Attribution
23
24	Bonnet–Chang, the sparse-cost sampling contradiction in Lemma 11.
25	-/
26
27	namespace Lax263307.CostSamplingObstruction
28
29	open Lax263307.GraphClasses Lax263307.InducedEmbeddingWidth Lax228581.Treewidth
30
31	axiom cost_width_obstruction {t n q : ℕ} (C : GraphClass) (hereditary : IsHereditary C)
32	(W : ℕ → ℕ) (monotone : Monotone W) (class_bound : HasBagBound C W)
33	(H : SimpleGraph (Fin t)) [DecidableRel H.Adj] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
34	(member : G ∈ C n) (D : Lax263307.RouteDistributions.Distribution G q) (hn : 0 < n)
35	(d L : ℕ) (degree_bound : ∀ v, H.degree v ≤ d) (edge_positive : 0 < H.edgeSet.ncard)
36	(x : Fin n → ℝ) (k ℓ p : ℝ) (k_positive : 0 < k) (ℓ_positive : 0 < ℓ) (p_positive : 0 < p)
37	(cost_bounds : ∀ v, 0 ≤ x v ∧ x v ≤ 1) (mass : (∑ v, x v) ≤ k)
38	(load_bound : ∀ v, Lax263307.PathSampling.load D.toSampling v ≤ ℓ * x v / k)
39	(edge_bound : Lax263307.Entropy.edgeCost G x ≤ k ^ 2 / p)
40	(target_large : 8 * (H.edgeSet.ncard : ℝ) ^ 2 * ℓ ^ 2 ≤ k)
41	(sparsity_large : 16 * (H.edgeSet.ncard : ℝ) ^ 2 * ℓ ^ 2 ≤ p) :
42	∃ removed : ℕ, (L : ℝ) * removed ≤ 4 * (H.edgeSet.ncard : ℝ) * ℓ ∧
43	treewidth H + 1 ≤ max 1 (2 * d * W (d * H.edgeSet.ncard * L ^ 2)) + removed
44
45	end Lax263307.CostSamplingObstruction
46

Show Proof

Formalization notes

The class bag bound is still an explicit intermediate hypothesis. This combines the proved probability estimates and sampled width obstruction; it does not yet derive the class bound from separators.

Attribution

Bonnet–Chang, the sparse-cost sampling contradiction in Lemma 11.

Builds on

Lax263307.InducedEmbeddingWidth

Used by

Lax263307.NoBoundedLoadRoutes

From Mathlib

none

Discussion

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

Loading discussion…

Lax Lean Archive

A width obstruction from sparse costs and bounded route loads

Flags

Flag this concept

Natural Language Statement

Theorem

Lean source view on GitHub

Attribution

Discussion

Settings

Your comments