Documentation

Complexitylib.Algebraic.LowerBound.Fusion.SumOfTerms.Waring.Translation.Binary

Binary-power compilation of Waring terms #

This contextual translation retains the shared linear-form computation from Waring.Translation.sharedTranslation, but replaces its linear-length power chain by the reusable binary-power DAG. Each source term therefore costs

2n + binaryMultiplicationCount (2n) + 1

multiplications: 2n coefficient products, a logarithmic power circuit, and one final scaling product.

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

One Waring-term gadget with a shared linear form and binary powering.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.termCircuit_size {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) :
    (termCircuit term).size = (linearFormExpression term).gateCount + (Arithmetic.Power.binaryCircuit (2 * n)).size + (scaleExpression term.scale).gateCount

    The gate count of termCircuit is the tree gate count of the linear form, plus the gate count of the binary power circuit, plus the tree gate count of the final scaling. Composing the stages adds no gates. Unlike the multiplication and addition charges below, the count includes the named-constant gates.

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

    Exact multiplication charge of the binary Waring-term gadget.

    Equations
    Instances For
      source
      def Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.termAdditionCount (n : ℕ) :
      ℕ

      Exact addition charge of the binary Waring-term gadget.

      Equations
      Instances For
        source
        @[simp]
        theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.termCircuit_multiplicationCost {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) :
        (termCircuit term).cost Arithmetic.multiplicationCost = termMultiplicationCount n
        source
        @[simp]
        theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.termCircuit_additionCost {K : Type} {n : ℕ} [Zero K] [One K] (term : Term K n) :
        (termCircuit term).cost Arithmetic.additionCost = termAdditionCount n
        source
        theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.eval_termCircuit {K : Type} {n : ℕ} [CommSemiring K] (term : Term K n) :
        (termCircuit term).eval (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X 0 = termValue term

        Binary term compilation preserves the charged power polynomial exactly.

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

        Contextual Waring translation using binary powering inside each term.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.pullCost_multiplicationCost {K : Type} [Semiring K] (n : ℕ) :
          (translation n).pullCost Arithmetic.multiplicationCost = SumOfTerms.weightedCost 0 (termMultiplicationCount n)

          Pulling multiplication cost through the binary translation charges only source terms, at their exact gadget cost.

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

          Pulling addition cost preserves source additions and charges the internal linear-form additions of every term.

          source
          theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.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 for binary Waring compilation.

          source
          theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.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 for binary Waring compilation.

          source
          theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.termMultiplicationCount_le (n : ℕ) (positive : 0 < n) :
          termMultiplicationCount n ≤ 2 * n + 2 * (2 * n).log2 + 1

          The binary term cost is linear in the number of variables plus a logarithmic powering overhead.

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

          Pulling polynomial semantics through binary compilation recovers the Waring sum-of-terms interpretation.

          source
          theorem Algebraic.Fusion.SumOfTerms.Waring.Translation.Binary.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 binary compilation preserves every Waring circuit's polynomial outputs.