Weighted support bounds across a circuit frontier

Opening a gate of arity at most weight + 1 increases the number of live wires by at most its weight. This bounds the union of the supports of any selected wires, including shared intermediate gates and free output wires.

def Cslib.Circuits.Program.frontierSupport {σ : Signature} {n g : ℕ} (program : Program σ n g) (frontier : Finset (Wire n g)) : Finset (Fin n)

The union of original inputs supporting a selected set of circuit wires.

Equations

• program.frontierSupport frontier = frontier.biUnion program.wireSupport

theorem Cslib.Circuits.Program.card_frontierSupport_le {σ : Signature} {n g : ℕ} (program : Program σ n g) (weight : Algebraic.OperationCost σ) (bounded : ∀ (op : σ.Op), σ.Arity op ≤ weight op + 1) (frontier : Finset (Wire n g)) : (program.frontierSupport frontier).card ≤ frontier.card + cost weight program

Weighted fan-in controls the number of inputs reaching an arbitrary wire frontier.