Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Forget

Forgetting the ports of witness variables #

A network over n + m variables reads its variables through ports. Forgetting the ports of the last m variables leaves a network over n variables with the same multigraph and the same local checks; an edge that carried a forgotten variable is now unconstrained. If the original network computes F, the forgotten network computes the existential projection x ↦ ∃ y, F (x, y): a satisfying assignment of the forgotten network reads off a witness from the forgotten port edges.

This is the only ingredient needed to transfer the cut-counting lower bound from deterministic to nondeterministic circuits, since the multigraph, and hence its cutwidth, is unchanged.

source
noncomputable def Algebraic.Cutwidth.Network.forget {n m : ℕ} {V E : Type} (N : Network (n + m) V E) :
Network n V E

Forget the ports of the last m variables. The multigraph and the local checks are unchanged; only the first n variables are read.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algebraic.Cutwidth.Network.mem_forget_read {n m : ℕ} {V E : Type} (N : Network (n + m) V E) {j : Fin n} :
    j ∈ N.forget.read ↔ Fin.castAdd m j ∈ N.read
    source
    @[simp]
    theorem Algebraic.Cutwidth.Network.forget_toMultigraph {n m : ℕ} {V E : Type} (N : Network (n + m) V E) :
    N.forget.toMultigraph = N.toMultigraph
    source
    @[simp]
    theorem Algebraic.Cutwidth.Network.forget_portEdge {n m : ℕ} {V E : Type} (N : Network (n + m) V E) (j : Fin n) :
    N.forget.portEdge j = N.portEdge (Fin.castAdd m j)
    source
    theorem Algebraic.Cutwidth.Network.card_forget_read_le {n m : ℕ} {V E : Type} (N : Network (n + m) V E) :
    N.forget.read.card ≤ N.read.card

    The forgotten network reads at most as many variables as the original.

    source
    theorem Algebraic.Cutwidth.Network.Computes.forget {n m : ℕ} {V E : Type} (N : Network (n + m) V E) {F : Cslib.BooleanFunction (n + m)} (h : N.Computes F) :
    N.forget.Computes fun (x : Cslib.BitString n) => decide (∃ (y : Fin m → Bool), F (Fin.append x y) = true)

    Forgetting witness ports computes the existential projection.