Pointwise charges for signed double-star weights

The energy of one edge is bounded by its center, crossing, or leak charges. This scalar partition argument is independent of graph Laplacians and can compile before their spectral infrastructure. Both double-star certificates use the same interior estimate.

theorem ACMax.Pointwise.square_charge_nonneg (condition : Prop) [Decidable condition] (weight : ℝ) : 0 ≤ if condition then weight ^ 2 else 0

Each conditional square is a nonnegative charge.

theorem ACMax.Pointwise.le_add_nonnegative_charges {left charge right value : ℝ} (hleft : 0 ≤ left) (hright : 0 ≤ right) (hvalue : value ≤ charge) : value ≤ left + charge + right

A charge is bounded by any nonnegative prefix and suffix added to it.

theorem ACMax.Pointwise.nonnegative_sub_sq_le {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a - b) ^ 2 ≤ a ^ 2 + b ^ 2

Same-sign nonnegative weights pay at most the sum of their squared charges.

theorem ACMax.Pointwise.double_star_edge_bound {V : Type u_1} (u v i j : V) (A B : Finset V) (au av : ℝ) (p q x : V → ℝ) (hp : ∀ w ∈ A, 0 ≤ p w) (hq : ∀ w ∈ B, 0 ≤ q w) (hAB : ∀ w ∈ A, w ∉ B) (hxu : x u = au) (hxv : x v = -av) (hxA : ∀ w ∈ A, x w = p w) (hxB : ∀ w ∈ B, x w = -q w) (hxZ : ∀ (w : V), w ≠ u → w ≠ v → w ∉ A → w ∉ B → x w = 0) (huj : i = u → j ∈ A) (hjuA : j = u → i ∈ A) (hvj : i = v → j ∈ B) (hjvB : j = v → i ∈ B) : (x i - x j) ^ 2 ≤ (((((((((if i = u then (au - p j) ^ 2 else 0) + if j = u then (au - p i) ^ 2 else 0) + if i = v then (av - q j) ^ 2 else 0) + if j = v then (av - q i) ^ 2 else 0) + if i ∈ A ∧ j ∈ B then (p i + q j) ^ 2 else 0) + if i ∈ B ∧ j ∈ A then (p j + q i) ^ 2 else 0) + if i ∈ A ∧ j ≠ u ∧ j ∉ B then p i ^ 2 else 0) + if j ∈ A ∧ i ≠ u ∧ i ∉ B then p j ^ 2 else 0) + if i ∈ B ∧ j ≠ v ∧ j ∉ A then q i ^ 2 else 0) + if j ∈ B ∧ i ≠ v ∧ i ∉ A then q j ^ 2 else 0

Bound one signed edge using two centers, two disjoint partner classes, and their leaks.