Absorbing arithmetic constants into polynomial coefficients

The compiler tracks an original wire either as a field constant or as a wire of the emitted program. Only addition and multiplication emit gates. Their constant operands are absorbed into the displayed bivariate polynomial.

@[reducible, inline]

abbrev Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.Ref (F : Type u_3) (n h : ℕ) : Type u_3

An eliminated constant or a retained signal.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.Ref F n h = (F ⊕ Cslib.Circuits.Wire n h)

def Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.value {F : Type u_1} {n h : ℕ} (values : Wire n h → F) : Ref F n h → F

Semantic value of a retained reference.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.value values = Sum.elim id values

def Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.wire {F : Type u_1} {n h : ℕ} (dummy : Fin n) : Ref F n h → Wire n h

Constants ignore their placeholder wire; other references use their retained wire.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.wire dummy (Sum.inl val) = Cslib.Circuits.Wire.input dummy
• Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.wire dummy (Sum.inr w) = w

noncomputable def Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.argument {F : Type u_1} [CommSemiring F] {n h : ℕ} (slot : Fin 2) : Ref F n h → MvPolynomial (Fin 2) F

A local argument becomes either a constant polynomial or the corresponding variable.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.argument slot (Sum.inl val) = MvPolynomial.C val
• Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.argument slot (Sum.inr w) = MvPolynomial.X slot

def Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.binary {F : Type u_1} [CommSemiring F] (add : Bool) (x y : F) : F

Interpret the addition/multiplication selector.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.binary add x y = if add = true then x + y else x * y

noncomputable def Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.binaryLine {F : Type u_1} [CommSemiring F] {n h : ℕ} (dummy : Fin n) (add : Bool) (args : Fin 2 → Ref F n h) : Line (signature F) n h

One emitted binary gate, with constants absorbed into its polynomial coefficients.

Equations

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

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.eval_argument {F : Type u_1} [CommSemiring F] {n h : ℕ} (dummy : Fin n) (args : Fin 2 → Ref F n h) (values : Wire n h → F) (slot : Fin 2) : (MvPolynomial.eval fun (i : Fin 2) => values (wire dummy (args i))) (argument slot (args slot)) = value values (args slot)

Substituting constants and variables recovers each original argument value.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.eval_binaryLine {F : Type u_1} [CommSemiring F] {n h : ℕ} (dummy : Fin n) (add : Bool) (args : Fin 2 → Ref F n h) (x : Fin n → F) (prior : Fin h → F) : (binaryLine dummy add args).eval (interpretation F) x prior = binary add (value (Wire.elim x prior) (args 0)) (value (Wire.elim x prior) (args 1))

The emitted gate has the same local arithmetic value.

def Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.liftRef {F : Type u_1} {n h : ℕ} : Ref F n h → Ref F n (h + 1)

Existing retained wires survive the insertion of one new gate.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.liftRef = Sum.map id Cslib.Circuits.Wire.castSucc

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.value_liftRef {F : Type u_1} [CommSemiring F] {n h : ℕ} (q : Program (signature F) n h) (line : Line (signature F) n h) (x : Fin n → F) (ref : Ref F n h) : value ((q.gate line).trace (interpretation F) x) (liftRef ref) = value (q.trace (interpretation F) x) ref

Lifting a reference preserves its value when extending the target program.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.exists_program {F : Type u_1} {K : Type u_2} [CommSemiring F] {n g : ℕ} (hn : 0 < n) (constant : K → F) (p : Program (Arithmetic.signature K) n g) : ∃ (h : ℕ) (q : Program (signature F) n h) (refs : Wire n g → Ref F n h), h = Program.cost Arithmetic.gateCost p ∧ q.FanInAtMost 2 ∧ ∀ (x : Fin n → F) (w : Wire n g), value (q.trace (interpretation F) x) (refs w) = p.trace (Arithmetic.interpretation constant) x w

Each arithmetic program has a polynomial realization with exactly its nonconstant cost.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.exists_circuit {F : Type u_1} {K : Type u_2} [CommSemiring F] {n : ℕ} (hn : 0 < n) (constant : K → F) {m : ℕ} (c : Circuit (Arithmetic.signature K) n m) (nonconstant : ∀ (j : Fin m), ∃ (x : Fin n → F) (y : Fin n → F), c.eval (Arithmetic.interpretation constant) x j ≠ c.eval (Arithmetic.interpretation constant) y j) : ∃ (d : Circuit (signature F) n m), d.size = c.cost Arithmetic.gateCost ∧ d.FanInAtMost 2 ∧ ∀ (x : Fin n → F), d.eval (interpretation F) x = c.eval (Arithmetic.interpretation constant) x

Nonconstant designated outputs use retained signals, so they need no final constant gates.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.ArithmeticInternal.outputs_nonconstant {F : Type u_3} {K : Type u_4} [Field F] {n : ℕ} (hn : 0 < n) (constant : K → F) (c : Circuit (Arithmetic.signature K) n n) {M : Matrix (Fin n) (Fin n) F} (regular : TotallyRegular M) (computes : c.Computes (Arithmetic.interpretation constant) fun (x : Fin n → F) => M.mulVec x) (i : Fin n) : ∃ (x : Fin n → F) (y : Fin n → F), c.eval (Arithmetic.interpretation constant) x i ≠ c.eval (Arithmetic.interpretation constant) y i

Every output of a nonempty totally regular linear map is nonconstant.