Documentation

Complexity.Computability.Circuit.Arithmetic.Power

Binary-power arithmetic circuits #

Binary powering computes each intermediate power once and shares it between the two inputs of a squaring gate. Every further binary digit adds one squaring and, for a one bit, a multiplication by the retained original input. A positive exponent e uses at most 2 * Nat.log2 e gates, all multiplications. Exponent zero uses a single named constant gate; exponent one uses only the input wire.

The constant symbol denoting one is an explicit parameter. Its interpretation is required to equal one only in the correctness theorem. Arbitrary weighted costs, including constant costs, are accounted for exactly. These are circuit-size results, not uniform TM-time certificates for circuit generation or evaluation.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Circuit.binaryPowerStep {C : Type v} (bit : Bool) (c : Circuit (arithSignature C) 1 1) :
Circuit (arithSignature C) 1 1

Add a binary digit to a shared power: square, then multiply by the original input for a one bit.

Instances For
    source
    def Cslib.Circuits.binaryPowerCircuit {C : Type v} (one : C) (e : ℕ) :
    Circuit (arithSignature C) 1 1

    Binary powering with a specified constant symbol for one.

    Instances For
      source
      def Cslib.Circuits.binaryMultiplicationCount (e : ℕ) :
      ℕ

      Exact multiplication count of binary powering: one squaring per nonleading bit and one further multiplication per nonleading one bit.

      Instances For
        source
        @[simp]
        theorem Cslib.Circuits.binaryPowerCircuit_zero {C : Type v} (one : C) :
        binaryPowerCircuit one 0 = Circuit.oneGate (ArithOp.const one) Fin.elim0
        source
        @[simp]
        theorem Cslib.Circuits.binaryPowerCircuit_one {C : Type v} (one : C) :
        binaryPowerCircuit one 1 = Circuit.id (arithSignature C) 1
        source
        @[simp]
        theorem Cslib.Circuits.binaryMultiplicationCount_zero :
        binaryMultiplicationCount 0 = 0
        source
        @[simp]
        theorem Cslib.Circuits.binaryMultiplicationCount_one :
        binaryMultiplicationCount 1 = 0
        source
        theorem Cslib.Circuits.binaryMultiplicationCount_bit (bit : Bool) (e : ℕ) (he : e ≠ 0) :
        binaryMultiplicationCount (Nat.bit bit e) = binaryMultiplicationCount e + 1 + bit.toNat
        source
        theorem Cslib.Circuits.eval_binaryPowerCircuit {C : Type v} {R : Type u} [Add R] [Monoid R] (one : C) (constant : C → R) (hone : constant one = 1) (e : ℕ) (x : Fin 1 → R) :
        (binaryPowerCircuit one e).eval (arithInterpretationWith C constant) x 0 = x 0 ^ e

        The circuit computes the natural power, including exponents zero and one.

        source
        theorem Cslib.Circuits.cost_program_binaryPowerCircuit {C : Type v} (one : C) (e : ℕ) (cost : ArithOp C → ℕ) :
        (binaryPowerCircuit one e).program.cost cost = if e = 0 then cost (ArithOp.const one) else binaryMultiplicationCount e * cost ArithOp.mul

        Exact weighted cost, charging the constant gate for exponent zero.

        source
        @[simp]
        theorem Cslib.Circuits.size_binaryPowerCircuit {C : Type v} (one : C) (e : ℕ) :
        (binaryPowerCircuit one e).size = if e = 0 then 1 else binaryMultiplicationCount e

        Every gate at a positive exponent is a multiplication; exponent zero has one constant.

        source
        theorem Cslib.Circuits.mulCost_binaryPowerCircuit {C : Type v} (one : C) (e : ℕ) :
        (binaryPowerCircuit one e).program.cost ArithOp.mulCost = binaryMultiplicationCount e

        The multiplication count includes multiplication by scalars.

        source
        theorem Cslib.Circuits.binaryMultiplicationCount_le_two_mul_log2 (e : ℕ) :
        binaryMultiplicationCount e ≤ 2 * e.log2

        Binary powering uses at most twice the base-two logarithm many multiplications.

        source
        theorem Cslib.Circuits.size_binaryPowerCircuit_le {C : Type v} (one : C) {e : ℕ} (he : 0 < e) :
        (binaryPowerCircuit one e).size ≤ 2 * e.log2

        A positive exponent needs at most 2 * log₂ e gates, all multiplications.