Compiling Waring sums to ordinary arithmetic circuits

A Waring term is syntactically nullary in the sum-of-terms basis but depends semantically on a shared family of polynomial variables. A contextual translation exposes those variables to every term gadget. The gadgets are compiled from reusable arithmetic expressions, giving exact semantics and a concrete ordinary arithmetic circuit for every sum-of-powers circuit.

def Algebraic.Fusion.SumOfTerms.Waring.Translation.expressionSum {K : Type} {variableCount : ℕ} [Zero K] : List (Arithmetic.Expression K variableCount) → Arithmetic.Expression K variableCount

Right-associated sum of arithmetic expressions, with a named zero for the empty sum.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Translation.expressionSum [] = Algebraic.Arithmetic.Expression.constant 0
• Algebraic.Fusion.SumOfTerms.Waring.Translation.expressionSum (expression :: expressions) = expression.add (Algebraic.Fusion.SumOfTerms.Waring.Translation.expressionSum expressions)

def Algebraic.Fusion.SumOfTerms.Waring.Translation.expressionPower {K : Type} {variableCount : ℕ} [One K] (base : Arithmetic.Expression K variableCount) : ℕ → Arithmetic.Expression K variableCount

Naive natural power expression. Tree compilation intentionally exposes every intermediate product as its own multiplication gate.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Translation.expressionPower base 0 = Algebraic.Arithmetic.Expression.constant 1
• Algebraic.Fusion.SumOfTerms.Waring.Translation.expressionPower base exponent.succ = base.mul (Algebraic.Fusion.SumOfTerms.Waring.Translation.expressionPower base exponent)

def Algebraic.Fusion.SumOfTerms.Waring.Translation.linearFormExpression {K : Type} {n : ℕ} [Zero K] (term : Term K n) : Arithmetic.Expression K (2 * n)

Arithmetic expression for the linear form of one Waring term.

Equations

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

def Algebraic.Fusion.SumOfTerms.Waring.Translation.termExpression {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) : Arithmetic.Expression K (2 * n)

Arithmetic expression for one charged Waring term.

Equations

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

def Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedPowerExpression {K : Type} [One K] (exponent : ℕ) : Arithmetic.Expression K 1

Power expression whose base arrives on one shared input wire. Unlike termExpression, tree compilation of this expression does not duplicate the linear-form computation.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedPowerExpression exponent = Algebraic.Fusion.SumOfTerms.Waring.Translation.expressionPower (Algebraic.Arithmetic.Expression.input 0) exponent

def Algebraic.Fusion.SumOfTerms.Waring.Translation.scaleExpression {K : Type} (scale : K) : Arithmetic.Expression K 1

Final scalar multiplication after a shared power computation.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Translation.scaleExpression scale = (Algebraic.Arithmetic.Expression.constant scale).mul (Algebraic.Arithmetic.Expression.input 0)

def Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedTermCircuit {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) : Circuit (Arithmetic.signature K) (2 * n) 1

DAG-style Waring-term gadget: compute the linear form once, feed its single output to a power chain, and apply the term scale once at the end.

Equations

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

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedTermCircuit_size {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) : (sharedTermCircuit term).size = (linearFormExpression term).gateCount + (sharedPowerExpression (2 * n)).gateCount + (scaleExpression term.scale).gateCount

The gate count of sharedTermCircuit is the sum of the tree gate counts of its three stages: the linear form, the shared power chain, and the final scaling. Composing the stages adds no gates. Unlike the multiplication and addition charges below, the count includes the named-constant gates.

def Algebraic.Fusion.SumOfTerms.Waring.Translation.additionExpression {K : Type} (n : ℕ) : Arithmetic.Expression K (2 * n + 2)

Arithmetic expression implementing the source addition gate after the 2n shared context inputs.

Equations

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.weightedCost_expressionSum {K : Type} {variableCount : ℕ} [Zero K] (addition multiplication : ℕ) (expressions : List (Arithmetic.Expression K variableCount)) : Arithmetic.Expression.weightedCost addition multiplication (expressionSum expressions) = (List.map (Arithmetic.Expression.weightedCost addition multiplication) expressions).sum + addition * expressions.length

A right-associated expression sum has the sum of its subtree costs plus one addition charge per list entry (including the final addition to zero).

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.weightedCost_expressionPower {K : Type} {variableCount : ℕ} [One K] (addition multiplication : ℕ) (base : Arithmetic.Expression K variableCount) (exponent : ℕ) : Arithmetic.Expression.weightedCost addition multiplication (expressionPower base exponent) = exponent * (Arithmetic.Expression.weightedCost addition multiplication base + multiplication)

Naive power compilation repeats the base tree once per exponent step and adds one multiplication node at that step.

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.multiplicationCount_linearFormExpression {K : Type} {n : ℕ} [Zero K] (term : Term K n) : (linearFormExpression term).multiplicationCount = 2 * n

Exact number of multiplications in a compiled linear-form gadget.

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.additionCount_linearFormExpression {K : Type} {n : ℕ} [Zero K] (term : Term K n) : (linearFormExpression term).additionCount = 2 * n

Exact number of additions in a compiled linear-form gadget.

def Algebraic.Fusion.SumOfTerms.Waring.Translation.termMultiplicationCount (n : ℕ) : ℕ

Multiplicative cost of one naive compiled Waring-term gadget.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Translation.termMultiplicationCount n = 2 * n * (2 * n + 1) + 1

def Algebraic.Fusion.SumOfTerms.Waring.Translation.termAdditionCount (n : ℕ) : ℕ

Additive cost of one naive compiled Waring-term gadget.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Translation.termAdditionCount n = 2 * n * (2 * n)

def Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedTermMultiplicationCount (n : ℕ) : ℕ

Multiplicative cost of one shared-linear-form Waring-term gadget.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedTermMultiplicationCount n = 4 * n + 1

def Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedTermAdditionCount (n : ℕ) : ℕ

Additive cost of one shared-linear-form Waring-term gadget.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedTermAdditionCount n = 2 * n

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.multiplicationCount_termExpression {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) : (termExpression term).multiplicationCount = termMultiplicationCount n

Exact multiplicative cost of a Waring-term expression.

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.additionCount_termExpression {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) : (termExpression term).additionCount = termAdditionCount n

Exact additive cost of a Waring-term expression.

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.multiplicationCount_additionExpression {K : Type} (n : ℕ) : (additionExpression n).multiplicationCount = 0

The source-addition gadget uses no multiplication gates.

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.additionCount_additionExpression {K : Type} (n : ℕ) : (additionExpression n).additionCount = 1

The source-addition gadget uses exactly one addition gate.

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedTermCircuit_multiplicationCost {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) : (sharedTermCircuit term).cost Arithmetic.multiplicationCost = sharedTermMultiplicationCount n

Exact multiplication cost of the shared term gadget.

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedTermCircuit_additionCost {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) : (sharedTermCircuit term).cost Arithmetic.additionCost = sharedTermAdditionCount n

Exact addition cost of the shared term gadget.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.eval_expressionSum {K : Type} {R : Type u_1} {variableCount : ℕ} [Semiring R] [Zero K] (constant : K → R) (input : Fin variableCount → R) (mapsZero : constant 0 = 0) (expressions : List (Arithmetic.Expression K variableCount)) : Arithmetic.Expression.eval constant input (expressionSum expressions) = (List.map (Arithmetic.Expression.eval constant input) expressions).sum

Evaluation of a right-associated expression sum.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.eval_expressionPower {K : Type} {R : Type u_1} {variableCount : ℕ} [Semiring R] [One K] (constant : K → R) (input : Fin variableCount → R) (mapsOne : constant 1 = 1) (base : Arithmetic.Expression K variableCount) (exponent : ℕ) : Arithmetic.Expression.eval constant input (expressionPower base exponent) = Arithmetic.Expression.eval constant input base ^ exponent

Evaluation of the naive power expression.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.eval_linearFormExpression {K : Type} {n : ℕ} [CommSemiring K] (term : Term K n) : Arithmetic.Expression.eval (⇑MvPolynomial.C) MvPolynomial.X (linearFormExpression term) = linearForm term

The linear-form expression evaluates to the polynomial linear form.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.eval_termExpression {K : Type} {n : ℕ} [CommSemiring K] (term : Term K n) : Arithmetic.Expression.eval (⇑MvPolynomial.C) MvPolynomial.X (termExpression term) = termValue term

The term expression evaluates exactly to the charged Waring term.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.eval_sharedTermCircuit {K : Type} {n : ℕ} [CommSemiring K] (term : Term K n) : (sharedTermCircuit term).eval (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X 0 = termValue term

The shared term gadget computes exactly the charged Waring term.

def Algebraic.Fusion.SumOfTerms.Waring.Translation.translation {K : Type} [Semiring K] (n : ℕ) : ContextualTranslation (SumOfTerms.signature (Term K n)) (Arithmetic.signature K) (2 * n)

Contextual compilation of Waring sum-of-terms syntax into the ordinary arithmetic basis.

Equations

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

def Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedTranslation {K : Type} [Semiring K] (n : ℕ) : ContextualTranslation (SumOfTerms.signature (Term K n)) (Arithmetic.signature K) (2 * n)

Contextual Waring translation using the shared-linear-form DAG gadget for each term.

Equations

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

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.pullCost_multiplicationCost {K : Type} [Semiring K] (n : ℕ) : (translation n).pullCost Arithmetic.multiplicationCost = SumOfTerms.weightedCost 0 (termMultiplicationCount n)

Pulling target multiplication cost through the Waring translation charges each source term by the exact naive term-gadget multiplication count and makes source addition free.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.pullCost_additionCost {K : Type} [Semiring K] (n : ℕ) : (translation n).pullCost Arithmetic.additionCost = SumOfTerms.weightedCost 1 (termAdditionCount n)

Pulling target addition cost through the Waring translation charges one for every source addition and charges each term by its exact internal addition count.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedPullCost_multiplicationCost {K : Type} [Semiring K] (n : ℕ) : (sharedTranslation n).pullCost Arithmetic.multiplicationCost = SumOfTerms.weightedCost 0 (sharedTermMultiplicationCount n)

The shared translation charges each source term by 4n+1 multiplications.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedPullCost_additionCost {K : Type} [Semiring K] (n : ℕ) : (sharedTranslation n).pullCost Arithmetic.additionCost = SumOfTerms.weightedCost 1 (sharedTermAdditionCount n)

The shared translation charges each term by 2n internal additions and preserves source additions one-for-one.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.compile_multiplicationCost {K : Type} {m : ℕ} [Semiring K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 m) : ((translation n).compile circuit).cost Arithmetic.multiplicationCost = circuit.cost (SumOfTerms.weightedCost 0 (termMultiplicationCount n))

Exact multiplication cost of contextual Waring compilation.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.compile_multiplicationCost_eq_termCost {K : Type} {m : ℕ} [Semiring K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 m) : ((translation n).compile circuit).cost Arithmetic.multiplicationCost = termMultiplicationCount n * circuit.cost SumOfTerms.termCost

Closed multiplication-cost formula: the naive compiler pays the same quadratic gadget cost for every Waring term and nothing for source addition.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.compile_additionCost {K : Type} {m : ℕ} [Semiring K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 m) : ((translation n).compile circuit).cost Arithmetic.additionCost = circuit.cost (SumOfTerms.weightedCost 1 (termAdditionCount n))

Exact addition cost of contextual Waring compilation.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.compile_additionCost_eq_sourceCosts {K : Type} {m : ℕ} [Semiring K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 m) : ((translation n).compile circuit).cost Arithmetic.additionCost = circuit.cost SumOfTerms.additionCost + termAdditionCount n * circuit.cost SumOfTerms.termCost

Closed addition-cost formula: source additions remain single additions, while each Waring term contributes its internal quadratic addition cost.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedCompile_multiplicationCost_eq_termCost {K : Type} {m : ℕ} [Semiring K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 m) : ((sharedTranslation n).compile circuit).cost Arithmetic.multiplicationCost = sharedTermMultiplicationCount n * circuit.cost SumOfTerms.termCost

Closed multiplication-cost formula for shared Waring compilation.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedCompile_additionCost_eq_sourceCosts {K : Type} {m : ℕ} [Semiring K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 m) : ((sharedTranslation n).compile circuit).cost Arithmetic.additionCost = circuit.cost SumOfTerms.additionCost + sharedTermAdditionCount n * circuit.cost SumOfTerms.termCost

Closed addition-cost formula for shared Waring compilation.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.pull_polynomial {K : Type} [CommSemiring K] (n : ℕ) : (translation n).pull (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X = SumOfTerms.interpretation termValue

Pulling ordinary polynomial semantics through the contextual translation recovers Waring sum-of-terms semantics exactly.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedPull_polynomial {K : Type} [CommSemiring K] (n : ℕ) : (sharedTranslation n).pull (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X = SumOfTerms.interpretation termValue

Pulling polynomial semantics through the shared-linear-form translation recovers Waring semantics exactly.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.compile_eval {K : Type} {m : ℕ} [CommSemiring K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 m) : ((translation n).compile circuit).eval (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X = circuit.eval (SumOfTerms.interpretation termValue) fun (input : Fin 0) => input.elim0

Contextual compilation preserves every Waring circuit's polynomial outputs.

theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.sharedCompile_eval {K : Type} {m : ℕ} [CommSemiring K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 m) : ((sharedTranslation n).compile circuit).eval (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X = circuit.eval (SumOfTerms.interpretation termValue) fun (input : Fin 0) => input.elim0

Shared-linear-form contextual compilation preserves every Waring circuit's polynomial outputs.