Reindexing the inputs read by an aggregate network

An equivalence enumerating the read variables turns a network on a subset of the original coordinates into a network reading all coordinates of a smaller cube. Graphs, local checks, contributions, and the final predicate are unchanged.

noncomputable def Algebraic.Cutwidth.AggregateNetwork.extendInput {n k : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) (e : Fin k ≃ ↥N.read) (outside : Fin n → Bool) (x : Fin k → Bool) (j : Fin n) : Bool

Extend the enumerated read variables, fixing all other coordinates.

Equations

• N.extendInput e outside x j = if h : j ∈ N.read then x (e.symm ⟨j, h⟩) else outside j

@[simp]

theorem Algebraic.Cutwidth.AggregateNetwork.extendInput_apply {n k : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) (e : Fin k ≃ ↥N.read) (outside : Fin n → Bool) (x : Fin k → Bool) (j : Fin k) : N.extendInput e outside x ↑(e j) = x j

noncomputable def Algebraic.Cutwidth.AggregateNetwork.reindex {n k : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) (e : Fin k ≃ ↥N.read) : AggregateNetwork k V E M

Enumerate the read variables without changing the graph or local data.

Equations

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

theorem Algebraic.Cutwidth.AggregateNetwork.reindex_toMultigraph {n k : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) (e : Fin k ≃ ↥N.read) : (N.reindex e).toMultigraph = N.toMultigraph

Input reindexing preserves the underlying multigraph.

@[simp]

theorem Algebraic.Cutwidth.AggregateNetwork.reindex_read {n k : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) (e : Fin k ≃ ↥N.read) : (N.reindex e).read = Finset.univ

theorem Algebraic.Cutwidth.AggregateNetwork.reindex_satisfies_iff {n k : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) (e : Fin k ≃ ↥N.read) [Fintype V] (x : Fin k → Bool) (y : Fin n → Bool) (hxy : ∀ (j : Fin k), y ↑(e j) = x j) (α : E → Bool) : (N.reindex e).Satisfies x α ↔ N.Satisfies y α

Satisfaction is preserved by the coordinate enumeration.

theorem Algebraic.Cutwidth.AggregateNetwork.reindex_computes {n k : ℕ} {V E M : Type} [CommMonoid M] (N : AggregateNetwork n V E M) (e : Fin k ≃ ↥N.read) [Fintype V] {f : Cslib.BooleanFunction n} (hf : N.Computes f) (outside : Fin n → Bool) : (N.reindex e).Computes fun (x : Cslib.BitString k) => f (N.extendInput e outside x)

The reindexed network computes the restriction obtained by fixing outside coordinates.