Constraint networks on trees of regions

Unique satisfying assignments make a laminar family of vertex separators coherent. The capacity of a merge is the union of its three boundaries, together with the inputs read at the merge. This construction assumes every input is read; unused inputs can be handled separately by the existing unused-input bias bound.

noncomputable def Complexity.Frontier.Network.boundaryValues {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (G : Network U ι V E) (X : Set V) (α : E → U) : E → Option U

Values on the boundary of an arbitrary vertex region.

Equations

• G.boundaryValues X α e = if e ∈ G.cut X then some (α e) else none

theorem Complexity.Frontier.Network.boundaryValues_eq_iff {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (G : Network U ι V E) (X : Set V) (α β : E → U) : G.boundaryValues X α = G.boundaryValues X β ↔ Set.EqOn α β (G.cut X)

def Complexity.Frontier.Network.readTree {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} {B : Type u_5} (G : Network U ι V E) (T : RegionTree V B) (hread : G.read = Set.univ) : RegionTree ι B

Transfer a decomposition of vertices to the inputs read in its regions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.Frontier.Network.treeFrontier {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} {B : Type u_5} (G : Network U ι V E) [Nonempty U] (T : RegionTree V B) (hread : G.read = Set.univ) : TreeFrontier G.accepted (E → Option U) B

A region tree gives network messages by restricting the canonical satisfying trace.

Equations

• G.treeFrontier T hread = { toRegionTree := G.readTree T hread, message := fun (v : B) (x : ι → U) => G.boundaryValues (T.region v) (G.witness x), message_root := ⋯, splice := ⋯ }

theorem Complexity.Frontier.Network.treeFrontier_coherent {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} {B : Type u_5} (G : Network U ι V E) [Nonempty U] (T : RegionTree V B) (hread : G.read = Set.univ) (hlam : ∀ (u v : B), T.region u ⊆ T.region v ∨ T.region v ⊆ T.region u ∨ Disjoint (T.region u) (T.region v)) (hunique : ∀ (x : ι → U) (α β : E → U), G.Satisfies x α → G.Satisfies x β → α = β) : (G.treeFrontier T hread).Coherent

Laminarity is what makes arbitrary region-state deletion preserve the network trace.

theorem Complexity.Frontier.Network.ncard_tree_transition_le {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} {B : Type u_5} (G : Network U ι V E) [Nonempty U] (T : RegionTree V B) (hread : G.read = Set.univ) [Finite ι] [Finite U] [Finite E] (v : B) : ((G.treeFrontier T hread).transition v '' G.accepted).ncard ≤ Nat.card U ^ ((G.cut (T.region v) ∪ G.cut (T.region (T.left v)) ∪ G.cut (T.region (T.right v))).ncard + ((G.treeFrontier T hread).localInputs v).ncard)

The number of joint merge states, with each edge in the boundary union paid once.

theorem Complexity.Frontier.Network.abs_sumOn_accepted_le_tree {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} {B : Type u_5} (G : Network U ι V E) [Nonempty U] (T : RegionTree V B) (hread : G.read = Set.univ) [Finite ι] [Finite U] [Finite E] [Fintype B] (hlam : ∀ (u v : B), T.region u ⊆ T.region v ∨ T.region v ⊆ T.region u ∨ Disjoint (T.region u) (T.region v)) (hunique : ∀ (x : ι → U) (α β : E → U), G.Satisfies x α → G.Satisfies x β → α = β) {K : ℕ} (hK : 1 < K) {w cost : (ι → U) → ℝ} {a : ℝ} (ha : 0 ≤ a) (hw : ∀ (x : ι → U), |w x| ≤ a) (hc : ∀ (x : ι → U), 0 ≤ cost x) (hrect : RectangleBudget w cost K K) : |sumOn w G.accepted| ≤ sumOn cost G.accepted + a * ↑((K - 1) ^ 3 * ∑ v : B, Nat.card U ^ ((G.cut (T.region v) ∪ G.cut (T.region (T.left v)) ∪ G.cut (T.region (T.right v))).ncard + ((G.treeFrontier T hread).localInputs v).ncard))

Weighted tree bound for networks. The exponent is the joint merge boundary, not the maximum of the three separate separator sizes.