Light adjacent pairs in weighted trees

Monien and Preis's red/black argument contracts parts of a black component to a weighted tree. When all its leaves are sufficiently heavy, a light adjacent pair gives the next small candidate for a positive set.

We prove their weighted-tree lemma through a forest inequality: nonnegative weights at leaves and isolated vertices, together with nonnegative sums across edges, force a nonnegative total. Shifting weights by a threshold then gives a light adjacent pair whenever the total lies below that threshold times the number of vertices. RedBlack.Restoration handles one local edge-restoration step. Monien and Preis's global tree reorganization is not formalized: RedBlack.Clusters proves their red/black lemma by bounded connected partitions instead, and Bisection.exists_bisectionBound uses it.

theorem Algebraic.Cutwidth.Bisection.WeightedTree.sum_nonneg_of_leaf_nonneg {W : Type} [Fintype W] (H : SimpleGraph W) (forest : H.IsAcyclic) (w : W → ℝ) (leaves : ∀ (v : W), H.degree v ≤ 1 → 0 ≤ w v) (edges : ∀ (u v : W), H.Adj u v → 0 ≤ w u + w v) : 0 ≤ ∑ v : W, w v

A finite forest has nonnegative total weight if its leaves and isolated vertices have nonnegative weight and every edge has nonnegative endpoint sum.

theorem Algebraic.Cutwidth.Bisection.WeightedTree.exists_adjacent_pair_lt_of_sum_lt {W : Type} [Fintype W] (H : SimpleGraph W) (forest : H.IsAcyclic) (w : W → ℝ) {A : ℝ} (leaves : ∀ (v : W), H.degree v ≤ 1 → A ≤ w v) (total : ∑ v : W, w v < A * ↑(Fintype.card W)) : ∃ (u : W) (v : W), H.Adj u v ∧ w u + w v < 2 * A

If leaves and isolated vertices weigh at least A, but the average weight is below A, some adjacent pair weighs less than 2 A.

theorem Algebraic.Cutwidth.Bisection.WeightedTree.exists_adjacent_pair_le {W : Type} [Fintype W] (H : SimpleGraph W) (tree : H.IsTree) (size : 1 < Fintype.card W) (w : W → ℕ) (leaves : ∀ (v : W), H.degree v = 1 → ∑ x : W, w x ≤ (Fintype.card W - 1) * w v) : ∃ (u : W) (v : W), H.Adj u v ∧ (Fintype.card W - 1) * (w u + w v) ≤ 2 * ∑ x : W, w x

Monien and Preis's weighted-tree lemma, with denominators cleared. In a tree on n ≥ 2 vertices, if every leaf weighs at least the total weight divided by n - 1, some adjacent pair weighs at most twice that ratio.