Constraint networks with a commutative aggregate

Local contributions multiply in a finite commutative monoid. The final acceptance predicate may inspect the product. No cancellation or inverses are required.

structure Algebraic.Cutwidth.AggregateNetwork (n : ℕ) (V E M : Type) [CommMonoid M] extends Algebraic.Cutwidth.Network n V E : Type

A local constraint network augmented with one commutative aggregate.

• fst : E → V
• snd : E → V
• Check : V → (E → Bool) → Prop
• check_local (v : V) (α β : E → Bool) : (∀ (e : E), self.fst e = v ∨ self.snd e = v → α e = β e) → self.Check v α → self.Check v β
• read : Finset (Fin n)
• portVertex : Fin n → V
• portEdge : Fin n → E
• port_incident (j : Fin n) : j ∈ self.read → self.fst (self.portEdge j) = self.portVertex j ∨ self.snd (self.portEdge j) = self.portVertex j
• contribution : V → (E → Bool) → M

  The contribution made at a vertex.

• contribution_local (v : V) (α β : E → Bool) : (∀ (e : E), self.fst e = v ∨ self.snd e = v → α e = β e) → self.contribution v α = self.contribution v β

  A contribution depends only on incident edge values.

• Accept : M → Prop

  The test on the final aggregate.

noncomputable def Algebraic.Cutwidth.AggregateNetwork.accumulated {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) (L : Finset V) (α : E → Bool) : M

Aggregate of contributions from a set of processed vertices.

Equations

• N.accumulated L α = ∏ v ∈ L, N.contribution v α

@[simp]

theorem Algebraic.Cutwidth.AggregateNetwork.accumulated_empty {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) (α : E → Bool) : N.accumulated ∅ α = 1

def Algebraic.Cutwidth.AggregateNetwork.Satisfies {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] (x : Fin n → Bool) (α : E → Bool) : Prop

A satisfying edge assignment obeys the local network and global aggregate test.

Equations

• N.Satisfies x α = (N.Satisfies x α ∧ N.Accept (N.accumulated Finset.univ α))

def Algebraic.Cutwidth.AggregateNetwork.Computes {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] (f : Cslib.BooleanFunction n) : Prop

The network accepts exactly the true inputs of the Boolean function.

Equations

• N.Computes f = ∀ (x : Cslib.BitString n), f x = true ↔ ∃ (α : E → Bool), N.Satisfies x α

noncomputable def Algebraic.Cutwidth.AggregateNetwork.pastSet {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] (L : Finset V) (σ : E → Bool) (m : M) : Finset (↥(N.past L) → Bool)

Past inputs compatible with a cut assignment and an exact past aggregate.

Equations

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

noncomputable def Algebraic.Cutwidth.AggregateNetwork.futureSet {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] (L : Finset V) (σ : E → Bool) (m : M) : Finset (↥(N.past L)ᶜ → Bool)

Future inputs compatible with the past aggregate and final acceptance.

Equations

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

theorem Algebraic.Cutwidth.AggregateNetwork.mem_pastSet {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] {L : Finset V} {σ : E → Bool} {m : M} {p : ↥(N.past L) → Bool} : p ∈ N.pastSet L σ m ↔ ∃ (α : E → Bool), (∀ v ∈ L, N.Check v α) ∧ (∀ e ∈ N.cut L, α e = σ e) ∧ (∀ (j : ↥(N.past L)), α (N.portEdge ↑j) = p j) ∧ N.accumulated L α = m

theorem Algebraic.Cutwidth.AggregateNetwork.mem_futureSet {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] {L : Finset V} {σ : E → Bool} {m : M} {q : ↥(N.past L)ᶜ → Bool} : q ∈ N.futureSet L σ m ↔ ∃ (β : E → Bool), (∀ v ∉ L, N.Check v β) ∧ (∀ e ∈ N.cut L, β e = σ e) ∧ (∀ (j : ↥(N.past L)ᶜ), ↑j ∈ N.read → β (N.portEdge ↑j) = q j) ∧ N.Accept (m * N.accumulated Lᶜ β)

theorem Algebraic.Cutwidth.AggregateNetwork.accumulated_mul_compl {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] (L : Finset V) (α : E → Bool) : N.accumulated L α * N.accumulated Lᶜ α = N.accumulated Finset.univ α

theorem Algebraic.Cutwidth.AggregateNetwork.pastSet_congr {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] {L : Finset V} {σ σ' : E → Bool} {m : M} (h : ∀ e ∈ N.cut L, σ e = σ' e) : N.pastSet L σ m = N.pastSet L σ' m

The past set uses only the edge values on the cut.

theorem Algebraic.Cutwidth.AggregateNetwork.futureSet_congr {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] {L : Finset V} {σ σ' : E → Bool} {m : M} (h : ∀ e ∈ N.cut L, σ e = σ' e) : N.futureSet L σ m = N.futureSet L σ' m

The future set uses only the edge values on the cut.

theorem Algebraic.Cutwidth.AggregateNetwork.restrict_mem_pastSet {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] {x : Fin n → Bool} {α : E → Bool} (h : N.Satisfies x α) (L : Finset V) : (fun (j : ↥(N.past L)) => x ↑j) ∈ N.pastSet L α (N.accumulated L α)

A satisfying input supplies a member of its own past set.

theorem Algebraic.Cutwidth.AggregateNetwork.restrict_mem_futureSet {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] {x : Fin n → Bool} {α : E → Bool} (h : N.Satisfies x α) (L : Finset V) : (fun (j : ↥(N.past L)ᶜ) => x ↑j) ∈ N.futureSet L α (N.accumulated L α)

A satisfying input supplies a member of its own future set.

theorem Algebraic.Cutwidth.AggregateNetwork.card_pastSet_empty_le {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] (σ : E → Bool) (m : M) : (N.pastSet ∅ σ m).card ≤ 1

The empty past has at most one assignment, for any aggregate.

theorem Algebraic.Cutwidth.AggregateNetwork.accepted_of_mem_pastSet_of_mem_futureSet {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [Fintype E] {f : Cslib.BooleanFunction n} (hf : N.Computes f) {L : Finset V} {σ : E → Bool} {m : M} {p : ↥(N.past L) → Bool} (hp : p ∈ N.pastSet L σ m) {q : ↥(N.past L)ᶜ → Bool} (hq : q ∈ N.futureSet L σ m) : f (glue (N.past L) p q) = true

Combining compatible sides is sound because contributions are local and commute.

theorem Algebraic.Cutwidth.AggregateNetwork.accumulated_upto {n : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) [Fintype V] [LinearOrder V] (v : V) (α : E → Bool) : N.accumulated (Network.upto v) α = N.accumulated (Network.below v) α * N.contribution v α

Advancing one vertex multiplies the accumulator by its local contribution.