Existentially hiding inputs

Network.hide existentially quantifies the last k inputs without changing the graph. Local witnesses can be assembled into one global witness because each input is read at a single site. No uniqueness of witnesses is assumed or needed.

def Complexity.Frontier.Network.hide {U : Type u_1} {V : Type u_2} {E : Type u_3} {n k : ℕ} (N : Network U (Fin (n + k)) V E) : Network U (Fin n) V E

Hide the last k inputs by existentially quantifying them in each local constraint.

Equations

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

theorem Complexity.Frontier.Network.satisfies_hide_iff {U : Type u_1} {V : Type u_2} {E : Type u_3} {n k : ℕ} (N : Network U (Fin (n + k)) V E) [Nonempty U] (x : Fin n → U) (α : E → U) : N.hide.Satisfies x α ↔ ∃ (y : Fin k → U), N.Satisfies (Fin.append x y) α

Local existential witnesses assemble into one assignment of the hidden inputs.

theorem Complexity.Frontier.Network.accepted_hide {U : Type u_1} {V : Type u_2} {E : Type u_3} {n k : ℕ} (N : Network U (Fin (n + k)) V E) [Nonempty U] : N.hide.accepted = {x : Fin n → U | ∃ (y : Fin k → U), Fin.append x y ∈ N.accepted}

Hiding inputs is exactly projection of the accepted set.

theorem Complexity.Frontier.Network.ncard_readAt_hide_le {U : Type u_1} {V : Type u_2} {E : Type u_3} {n k : ℕ} (N : Network U (Fin (n + k)) V E) (v : V) : (N.hide.readAt v).ncard ≤ (N.readAt v).ncard

The visible inputs read at a vertex inject into its original inputs.

theorem Complexity.Frontier.Network.ncard_read_hide_le {U : Type u_1} {V : Type u_2} {E : Type u_3} {n k : ℕ} (N : Network U (Fin (n + k)) V E) : N.hide.read.ncard ≤ N.read.ncard

Hiding inputs can only reduce the number of inputs read.