Finite counting for an observed circuit component

A connected closed component with at least two inputs has an exact monoid-network compiler. Reindexing those inputs and applying a graph ordering gives the finite acceptance bound, with one multiplicative factor for the aggregate state space.

noncomputable def Algebraic.Cutwidth.Aggregate.componentFunction {σ : Signature} {n g m : ℕ} {p : Program σ n g} (K : MultiOutput.Internal.ClosedSet p) (I : Interpretation σ Bool) {M : Type} [CommMonoid M] (φ : MultiOutput.Internal.WireGraph.Signal K → Bool → M) (Accept : M → Prop) (e : Fin m ≃ ↥(SingleCut.inputsIn K.carrier)) (outside : Fin n → Bool) : Cslib.BooleanFunction m

The predicate obtained by observing every signal of a component, with outside inputs fixed and its own input coordinates enumerated by e.

Equations

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

theorem Algebraic.Cutwidth.Aggregate.card_componentFunction_le {σ : Signature} {n g m : ℕ} {p : Program σ n g} (K : MultiOutput.Internal.ClosedSet p) (I : Interpretation σ Bool) {M : Type} [CommMonoid M] [Fintype M] (φ : MultiOutput.Internal.WireGraph.Signal K → Bool → M) (Accept : M → Prop) (e : Fin m ≃ ↥(SingleCut.inputsIn K.carrier)) (outside : Fin n → Bool) (hp : p.FanInAtMost 2) (hm : 2 ≤ m) (hconn : ∀ u ∈ K.carrier, ∀ v ∈ K.carrier, Relation.ReflTransGen (MultiOutput.Linked p) u v) {A η C : ℝ} (hAη : 0 ≤ A + η) (hC : 0 ≤ C) (order : Multigraph.OrderingBound A η C) {Krect : ℕ} (hK : 1 < Krect) (hrect : RectangleFree (componentFunction K I φ Accept e outside) Krect) : ↑(accepting (componentFunction K I φ Accept e outside)).card ≤ ((↑n + 3 * ↑g) * 2 ^ ((A + η) * max (↑g - ↑m) 0 + 3 * Real.logb 2 (↑n + 3 * ↑g) + C + 3) + 1) * ↑(Fintype.card M) * ↑Krect ^ 2

A closed connected fan-in-two component has the finite aggregate counting bound. The ambient gate count bounds selected gates; no assumption on the predicate is used except rectangle-freeness of the resulting restricted function.

theorem Algebraic.Cutwidth.Aggregate.card_restriction_le {n g m : ℕ} {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] (p : Program (Aggregate.signature State) n g) (out : Wire n g) (a₀ : Aggregate.Guess p) (K : MultiOutput.Internal.ClosedSet (Aggregate.erase p a₀)) (e : Fin m ≃ ↥(SingleCut.inputsIn K.carrier)) (outside : Fin n → Bool) (hm : 2 ≤ m) (hconn : ∀ u ∈ K.carrier, ∀ v ∈ K.carrier, Relation.ReflTransGen (MultiOutput.Linked (Aggregate.erase p a₀)) u v) {A η C : ℝ} (hAη : 0 ≤ A + η) (hC : 0 ≤ C) (order : Multigraph.OrderingBound A η C) {Krect : ℕ} (hK : 1 < Krect) (hrect : RectangleFree (fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out) Krect) : ↑(accepting (restriction (fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out) (SingleCut.inputsIn K.carrier) e.symm outside)).card ≤ ((↑n + 3 * ↑g) * 2 ^ ((A + η) * max (↑g - ↑m) 0 + 3 * Real.logb 2 (↑n + 3 * ↑g) + C + 3) + 1) * 2 ^ (Aggregate.budget p + 1) * ↑Krect ^ 2

Summing exact guessed computations multiplies the component bound by at most 2 ^ (budget + 1). The one extra bit observes the designated output without an edge.