Coherent frontier traces of unambiguous networks

Uniqueness of satisfying edge assignments makes the separator lemma splice the entire frontier trace. This supplies the stronger interface needed by weighted peeling.

theorem Complexity.Frontier.Network.sweep_coherent {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) [Nonempty U] (hunique : ∀ (x : ι → U) (α β : E → U), N.Satisfies x α → N.Satisfies x β → α = β) : (N.sweep π).Coherent

The sweep of a network with unique satisfying assignments preserves entire traces.

theorem Complexity.Frontier.Network.transitionCount_sweep_le {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) [Nonempty U] [Finite ι] [Finite U] [Finite E] {w d m : ℕ} (hw : ∀ (t : ℕ), (N.frontier π t).ncard ≤ w) (hd : N.MaxDegreeLE d) (hm : ∀ (v : V), (N.readAt v).ncard ≤ m) : (N.sweep π).transitionCount ≤ Nat.card V * Nat.card U ^ (w + d + m) + Nat.card U ^ N.readᶜ.ncard

The transition bound is independent of any rectangle or weight hypothesis.

theorem Complexity.Frontier.Network.abs_sumOn_accepted_le {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) [Nonempty U] [Finite ι] [Finite U] [Finite E] (hunique : ∀ (x : ι → U) (α β : E → U), N.Satisfies x α → N.Satisfies x β → α = β) {KL KR : ℕ} (hKL : 1 < KL) (hKR : 1 < KR) {weight cost : (ι → U) → ℝ} {a : ℝ} (ha : 0 ≤ a) (hweight : ∀ (x : ι → U), |weight x| ≤ a) (hc : ∀ (x : ι → U), 0 ≤ cost x) (hrect : RectangleBudget weight cost KL KR) {w d m : ℕ} (hw : ∀ (t : ℕ), (N.frontier π t).ncard ≤ w) (hd : N.MaxDegreeLE d) (hm : ∀ (v : V), (N.readAt v).ncard ≤ m) : |sumOn weight N.accepted| ≤ sumOn cost N.accepted + a * ↑((KL - 1) * (KR - 1) * (Nat.card V * Nat.card U ^ (w + d + m) + Nat.card U ^ N.readᶜ.ncard))

Weighted peeling applied to the uniquely determined runs of a network.