Compiling Waring circuits to arithmetic circuits

Each Waring term computes its linear form once, raises the result by binary powering, and multiplies by its scale. Generic formulas compile the linear form and scaling; circuit composition preserves sharing through the power computation. Contextual simulation then makes the same variable block available to every term gadget and preserves every source output.

The construction accepts arbitrary coefficient symbols, with explicit symbols for zero and one. Correctness requires their interpretations to be zero and one. Costs count all generated gates, including unused source gates, coefficient constants and the initial zero. Multiplication and addition counts specialize the exact arbitrary-weight formula. These are circuit costs, not TM-time certificates for generating or evaluating encoded circuits, and no optimality of the construction is asserted.

Main definitions

• Cslib.Circuits.Waring.Term.toCircuit: linear form, binary power and final scaling.
• Cslib.Circuits.Waring.compile: compile a sum-of-terms circuit with shared variable inputs.
• Cslib.Circuits.Waring.compilationCost: the exact charge of each source operation.

Main results

• Cslib.Circuits.Waring.eval_compile: all outputs agree under a semiring interpretation.
• Cslib.Circuits.Waring.polynomial_compile: equality of formal polynomial outputs.
• Cslib.Circuits.Waring.cost_program_compile: exact arbitrary weighted cost.
• Cslib.Circuits.Waring.mulCost_compile, Cslib.Circuits.Waring.addCost_compile, Cslib.Circuits.Waring.size_compile: closed multiplication, addition and gate counts.

References

• Adapted from LowerBound/Fusion/SumOfTerms/Waring/Translation.lean and its Binary.lean extension in S. Schlesinger, Algebraic circuit formalizations in Complexitylib. The source's separate arithmetic expression and contextual translation frameworks are replaced by the shared formula and circuit APIs.

def Cslib.Circuits.Waring.Term.toCircuit {C : Type v} {d : ℕ} (zero one : C) (t : Term C d) : Circuit (arithSignature C) d 1

Compute the linear form once, use a binary-power DAG, and apply the scale once.

theorem Cslib.Circuits.Waring.Term.eval_toCircuit {C : Type v} {R : Type u} {d : ℕ} [Semiring R] (zero one : C) (constant : C → R) (hzero : constant zero = 0) (hone : constant one = 1) (t : Term C d) (x : Fin d → R) : (toCircuit zero one t).eval (arithInterpretationWith C constant) x 0 = t.eval constant x

Term compilation preserves evaluation under any semiring interpretation of the symbols.

theorem Cslib.Circuits.Waring.Term.cost_program_toCircuit {C : Type v} {d : ℕ} (zero one : C) (weight : ArithOp C → ℕ) (t : Term C d) : (toCircuit zero one t).program.cost weight = (weight (ArithOp.const zero) + ∑ i : Fin d, (weight (ArithOp.const (t.coefficients i)) + weight ArithOp.mul + weight ArithOp.add) + if d = 0 then weight (ArithOp.const one) else binaryMultiplicationCount d * weight ArithOp.mul) + (weight (ArithOp.const t.scale) + weight ArithOp.mul)

Exact weighted term cost, including all coefficient and zero/one constants.

def Cslib.Circuits.Waring.termMultiplicationCount (d : ℕ) : ℕ

The multiplication count of a compiled term, including coefficient and scale products.

theorem Cslib.Circuits.Waring.Term.mulCost_toCircuit {C : Type v} {d : ℕ} (zero one : C) (t : Term C d) : (toCircuit zero one t).program.cost ArithOp.mulCost = termMultiplicationCount d

Exact term multiplication count, including the final scale multiplication at degree zero.

theorem Cslib.Circuits.Waring.Term.addCost_toCircuit {C : Type v} {d : ℕ} (zero one : C) (t : Term C d) : (toCircuit zero one t).program.cost ArithOp.addCost = d

There is one linear-form addition per variable, including the initial addition to zero.

theorem Cslib.Circuits.Waring.Term.size_toCircuit {C : Type v} {d : ℕ} (zero one : C) (t : Term C d) : (toCircuit zero one t).size = (3 * d + if d = 0 then 1 else binaryMultiplicationCount d) + 3

The total gate count includes coefficient constants, zero, scaling, and the power circuit.

theorem Cslib.Circuits.Waring.termMultiplicationCount_le (d : ℕ) : termMultiplicationCount d ≤ d + 2 * d.log2 + 1

Binary powering adds at most twice the binary logarithm to the linear-form cost. This includes degree zero, where only the final scale multiplication is charged.

def Cslib.Circuits.Waring.operationCircuit {C : Type v} (zero one : C) (d : ℕ) (op : SumOfTerms.Op (Term C d)) : Circuit (arithSignature C) (d + op.arity) 1

One arithmetic gadget for a source operation, reading variables before source arguments.

def Cslib.Circuits.Waring.compile {C : Type v} {d n m : ℕ} (zero one : C) (c : Circuit (SumOfTerms.signature (Term C d)) n m) : Circuit (arithSignature C) (d + n) m

Compile every source operation, sharing the first d inputs as the variable context. Any original inputs follow that context and remain available to the source program.

theorem Cslib.Circuits.Waring.eval_compile {C : Type v} {R : Type u} {d n m : ℕ} [Semiring R] (zero one : C) (constant : C → R) (hzero : constant zero = 0) (hone : constant one = 1) (c : Circuit (SumOfTerms.signature (Term C d)) n m) (x : Fin d → R) (y : Fin n → R) : (compile zero one c).eval (arithInterpretationWith C constant) (Fin.append x y) = c.eval (SumOfTerms.interpretation fun (t : Term C d) => t.eval constant x) y

Interpret the shared variables and preserve all source outputs, including supplied inputs.

theorem Cslib.Circuits.Waring.polynomial_compile {d m : ℕ} {K : Type u_1} [CommSemiring K] (c : Circuit (SumOfTerms.signature (Term K d)) 0 m) : (compile 0 1 c).eval (arithInterpretationWith K ⇑MvPolynomial.C) MvPolynomial.X = c.eval (SumOfTerms.interpretation Term.polynomial) Fin.elim0

Compiling a closed Waring circuit preserves equality of formal polynomials at every output.

def Cslib.Circuits.Waring.compilationCost {C : Type v} {d : ℕ} (zero one : C) (weight : ArithOp C → ℕ) : SumOfTerms.Op (Term C d) → ℕ

The complete generated cost of each source operation, with arbitrary constant weights.

theorem Cslib.Circuits.Waring.cost_program_compile {C : Type v} {d n m : ℕ} (zero one : C) (c : Circuit (SumOfTerms.signature (Term C d)) n m) (weight : ArithOp C → ℕ) : (compile zero one c).program.cost weight = c.program.cost (compilationCost zero one weight)

Every source gate is charged exactly once, including gates unused by the chosen outputs.

theorem Cslib.Circuits.Waring.cost_program_compile_of_termCost {C : Type v} {d n m : ℕ} (zero one : C) (c : Circuit (SumOfTerms.signature (Term C d)) n m) (weight : ArithOp C → ℕ) {term : ℕ} (hterm : ∀ (t : Term C d), (Term.toCircuit zero one t).program.cost weight = term) : (compile zero one c).program.cost weight = weight ArithOp.add * c.program.cost SumOfTerms.addCost + term * c.program.cost SumOfTerms.termCost

Uniform term costs separate the total charge into source additions and term gates.

theorem Cslib.Circuits.Waring.mulCost_compile {C : Type v} {d n m : ℕ} (zero one : C) (c : Circuit (SumOfTerms.signature (Term C d)) n m) : (compile zero one c).program.cost ArithOp.mulCost = termMultiplicationCount d * c.program.cost SumOfTerms.termCost

Multiplications are exactly the per-term count times the number of source term gates.

theorem Cslib.Circuits.Waring.addCost_compile {C : Type v} {d n m : ℕ} (zero one : C) (c : Circuit (SumOfTerms.signature (Term C d)) n m) : (compile zero one c).program.cost ArithOp.addCost = c.program.cost SumOfTerms.addCost + d * c.program.cost SumOfTerms.termCost

Source additions remain, and every term contributes its d linear-form additions.

theorem Cslib.Circuits.Waring.size_compile {C : Type v} {d n m : ℕ} (zero one : C) (c : Circuit (SumOfTerms.signature (Term C d)) n m) : (compile zero one c).size = c.program.cost SumOfTerms.addCost + ((3 * d + if d = 0 then 1 else binaryMultiplicationCount d) + 3) * c.program.cost SumOfTerms.termCost

The full gate count, including constants and source gates unused by the outputs.