Local linear realizations of a program

A realization assigns a coefficient row to every original circuit wire. Inputs carry the standard coordinate rows, and each gate row belongs to the linear span of its original argument rows. The field may be finite or infinite.

structure Algebraic.Cutwidth.MultiOutput.Linear.Realization {σ : Signature} {n s : ℕ} (p : Program σ n s) (F : Type u_1) [Field F] : Type u_1

A coefficient certificate that respects the original program's local dependencies.

• value : Wire n s → Fin n → F

  The linear coefficient row carried by each original wire.

• input (j : Fin n) : self.value (Wire.input j) = Pi.single j 1

  Primary inputs carry their standard coordinate rows.

• gate (g : Fin s) : self.value (Wire.gate g) ∈ Submodule.span F (Set.range fun (i : Fin (σ.Arity (p.lines g).op)) => self.value ((p.lines g).wires i))

  Every gate row is generated by the rows on its original input slots.