Hiding the inputs of a constraint network

A constraint network on the inputs ι ⊕ κ hides the inputs in κ (Network.hide) by quantifying them existentially in each local constraint, on the same multigraph. Since each hidden input is read at no more than one vertex, local witnesses for the hidden inputs assemble into one global witness (Network.satisfies_hide_iff). So the hidden network accepts exactly the projection of the accepted set (Network.accepted_hide). Witnesses need not be unique.

Hiding keeps the multigraph, and with it every degree, frontier and width; it only forgets the hidden inputs, so it reads no more inputs than before. Inputs can also be renamed along an equivalence (Network.reindex), for instance to hide the last k of n + k inputs.

Main definitions

• Cslib.Circuits.Frontier.Network.reindex: renaming the inputs of a network.
• Cslib.Circuits.Frontier.Network.hide: hiding the inputs in κ of a network on ι ⊕ κ.

Main results

• Cslib.Circuits.Frontier.Network.accepted_reindex: renaming the inputs renames the accepted set.
• Cslib.Circuits.Frontier.Network.satisfies_hide_iff: local witnesses assemble into a global one.
• Cslib.Circuits.Frontier.Network.accepted_hide: hiding inputs projects the accepted set.
• Cslib.Circuits.Frontier.Network.ncard_readAt_hide_le, Cslib.Circuits.Frontier.Network.ncard_read_hide_le: hiding inputs reads fewer inputs.

Renaming inputs

def Cslib.Circuits.Frontier.Network.reindex {U : Type u_1} {ι : Type u_2} {ι' : Type u_3} {V : Type u_5} {E : Type u_6} (N : Network U ι V E) (e : ι ≃ ι') : Network U ι' V E

Rename the inputs of a network along an equivalence e : ι ≃ ι': the input e i is read where i was, and the constraints see an input x on ι' as the input x ∘ e on ι.

@[simp]

theorem Cslib.Circuits.Frontier.Network.reindex_toMultigraph {U : Type u_1} {ι : Type u_2} {ι' : Type u_3} {V : Type u_5} {E : Type u_6} (N : Network U ι V E) (e : ι ≃ ι') : (N.reindex e).toMultigraph = N.toMultigraph

theorem Cslib.Circuits.Frontier.Network.satisfies_reindex_iff {U : Type u_1} {ι : Type u_2} {ι' : Type u_3} {V : Type u_5} {E : Type u_6} (N : Network U ι V E) (e : ι ≃ ι') {x : ι' → U} {α : E → U} : (N.reindex e).Satisfies x α ↔ N.Satisfies (x ∘ ⇑e) α

theorem Cslib.Circuits.Frontier.Network.accepted_reindex {U : Type u_1} {ι : Type u_2} {ι' : Type u_3} {V : Type u_5} {E : Type u_6} (N : Network U ι V E) (e : ι ≃ ι') : (N.reindex e).accepted = {x : ι' → U | x ∘ ⇑e ∈ N.accepted}

Renaming the inputs renames the accepted set.

theorem Cslib.Circuits.Frontier.Network.readAt_reindex {U : Type u_1} {ι : Type u_2} {ι' : Type u_3} {V : Type u_5} {E : Type u_6} (N : Network U ι V E) (e : ι ≃ ι') (v : V) : (N.reindex e).readAt v = ⇑e '' N.readAt v

theorem Cslib.Circuits.Frontier.Network.read_reindex {U : Type u_1} {ι : Type u_2} {ι' : Type u_3} {V : Type u_5} {E : Type u_6} (N : Network U ι V E) (e : ι ≃ ι') : (N.reindex e).read = ⇑e '' N.read

@[simp]

theorem Cslib.Circuits.Frontier.Network.ncard_readAt_reindex {U : Type u_1} {ι : Type u_2} {ι' : Type u_3} {V : Type u_5} {E : Type u_6} (N : Network U ι V E) (e : ι ≃ ι') (v : V) : ((N.reindex e).readAt v).ncard = (N.readAt v).ncard

@[simp]

theorem Cslib.Circuits.Frontier.Network.ncard_read_reindex {U : Type u_1} {ι : Type u_2} {ι' : Type u_3} {V : Type u_5} {E : Type u_6} (N : Network U ι V E) (e : ι ≃ ι') : (N.reindex e).read.ncard = N.read.ncard

Hiding inputs

def Cslib.Circuits.Frontier.Network.hide {U : Type u_1} {ι : Type u_2} {κ : Type u_4} {V : Type u_5} {E : Type u_6} (N : Network U (ι ⊕ κ) V E) : Network U ι V E

Hiding inputs. The network on the inputs ι obtained from a network on ι ⊕ κ by quantifying the inputs in κ existentially in each local constraint, on the same multigraph. The visible inputs are read where they were.

@[simp]

theorem Cslib.Circuits.Frontier.Network.hide_toMultigraph {U : Type u_1} {ι : Type u_2} {κ : Type u_4} {V : Type u_5} {E : Type u_6} (N : Network U (ι ⊕ κ) V E) : N.hide.toMultigraph = N.toMultigraph

theorem Cslib.Circuits.Frontier.Network.satisfies_hide_iff {U : Type u_1} {ι : Type u_2} {κ : Type u_4} {V : Type u_5} {E : Type u_6} (N : Network U (ι ⊕ κ) V E) [Nonempty U] {x : ι → U} {α : E → U} : N.hide.Satisfies x α ↔ ∃ (y : κ → U), N.Satisfies (Sum.elim x y) α

Local witnesses assemble into a global one. An assignment satisfies the hidden network on x exactly when it satisfies the original network on x and some values of the hidden inputs. Each hidden input is read at no more than one vertex, so it takes the value that the witness of that vertex gives it.

theorem Cslib.Circuits.Frontier.Network.accepted_hide {U : Type u_1} {ι : Type u_2} {κ : Type u_4} {V : Type u_5} {E : Type u_6} (N : Network U (ι ⊕ κ) V E) [Nonempty U] : N.hide.accepted = {x : ι → U | ∃ (y : κ → U), Sum.elim x y ∈ N.accepted}

Hiding inputs projects the accepted set.

theorem Cslib.Circuits.Frontier.Network.readAt_hide {U : Type u_1} {ι : Type u_2} {κ : Type u_4} {V : Type u_5} {E : Type u_6} (N : Network U (ι ⊕ κ) V E) (v : V) : N.hide.readAt v = Sum.inl ⁻¹' N.readAt v

theorem Cslib.Circuits.Frontier.Network.read_hide {U : Type u_1} {ι : Type u_2} {κ : Type u_4} {V : Type u_5} {E : Type u_6} (N : Network U (ι ⊕ κ) V E) : N.hide.read = Sum.inl ⁻¹' N.read

theorem Cslib.Circuits.Frontier.Network.ncard_readAt_hide_le {U : Type u_1} {ι : Type u_2} {κ : Type u_4} {V : Type u_5} {E : Type u_6} (N : Network U (ι ⊕ κ) V E) (v : V) (hv : (N.readAt v).Finite := by toFinite_tac) : (N.hide.readAt v).ncard ≤ (N.readAt v).ncard

The visible inputs read at a vertex are among the inputs it read before hiding.

theorem Cslib.Circuits.Frontier.Network.ncard_read_hide_le {U : Type u_1} {ι : Type u_2} {κ : Type u_4} {V : Type u_5} {E : Type u_6} (N : Network U (ι ⊕ κ) V E) (hN : N.read.Finite := by toFinite_tac) : N.hide.read.ncard ≤ N.read.ncard

Hiding inputs can only decrease the number of inputs read.