Shared arithmetic power circuits

Binary powering is a small but important reusable DAG primitive. Unlike a tree expression for repeated multiplication, each recursively computed power is shared by the squaring gate. For positive exponent e, the resulting number of multiplication gates is at most 2 * Nat.log2 e.

def Algebraic.Arithmetic.Power.squareCircuit {K : Type} (circuit : Circuit (signature K) 1 1) : Circuit (signature K) 1 1

Append one gate that squares the output of a one-output circuit.

Equations

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

def Algebraic.Arithmetic.Power.multiplyInputCircuit {K : Type} (circuit : Circuit (signature K) 1 1) : Circuit (signature K) 1 1

Append one gate that multiplies a circuit's output by its original input. The original input remains available because programs retain their input-wire namespace.

Equations

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

@[simp]

theorem Algebraic.Arithmetic.Power.size_squareCircuit {K : Type} (circuit : Circuit (signature K) 1 1) : (squareCircuit circuit).size = circuit.size + 1

Squaring appends exactly one gate.

@[simp]

theorem Algebraic.Arithmetic.Power.size_multiplyInputCircuit {K : Type} (circuit : Circuit (signature K) 1 1) : (multiplyInputCircuit circuit).size = circuit.size + 1

Multiplication by the retained input appends exactly one gate.

theorem Algebraic.Arithmetic.Power.squareCircuit_eval {K R : Type} [Add R] [Mul R] (constant : K → R) (input : Fin 1 → R) (circuit : Circuit (signature K) 1 1) : (squareCircuit circuit).eval (interpretation constant) input 0 = circuit.eval (interpretation constant) input 0 * circuit.eval (interpretation constant) input 0

Squaring has the expected semantics.

theorem Algebraic.Arithmetic.Power.multiplyInputCircuit_eval {K R : Type} [Add R] [Mul R] (constant : K → R) (input : Fin 1 → R) (circuit : Circuit (signature K) 1 1) : (multiplyInputCircuit circuit).eval (interpretation constant) input 0 = circuit.eval (interpretation constant) input 0 * input 0

Multiplication by the retained input has the expected semantics.

@[simp]

theorem Algebraic.Arithmetic.Power.squareCircuit_multiplicationCost {K : Type} (circuit : Circuit (signature K) 1 1) : (squareCircuit circuit).cost multiplicationCost = circuit.cost multiplicationCost + 1

Squaring adds exactly one multiplication to the circuit cost.

@[simp]

theorem Algebraic.Arithmetic.Power.multiplyInputCircuit_multiplicationCost {K : Type} (circuit : Circuit (signature K) 1 1) : (multiplyInputCircuit circuit).cost multiplicationCost = circuit.cost multiplicationCost + 1

Multiplication by the retained input adds exactly one multiplication.

@[simp]

theorem Algebraic.Arithmetic.Power.squareCircuit_additionCost {K : Type} (circuit : Circuit (signature K) 1 1) : (squareCircuit circuit).cost additionCost = circuit.cost additionCost

Squaring introduces no addition cost.

@[simp]

theorem Algebraic.Arithmetic.Power.multiplyInputCircuit_additionCost {K : Type} (circuit : Circuit (signature K) 1 1) : (multiplyInputCircuit circuit).cost additionCost = circuit.cost additionCost

Multiplication by the retained input introduces no addition cost.

def Algebraic.Arithmetic.Power.binaryCircuit {K : Type} [One K] (exponent : ℕ) : Circuit (signature K) 1 1

A shared binary-power circuit; its gate count is the bundled size. Zero uses one free constant gate; one is the zero-gate identity; each further binary digit contributes one squaring and, for a one bit, one multiplication by the retained input.

Equations

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

def Algebraic.Arithmetic.Power.binaryPowerGateCount {K : Type} [One K] (exponent : ℕ) : ℕ

Gate count of the binary-power circuit.

Equations

• Algebraic.Arithmetic.Power.binaryPowerGateCount exponent = (Algebraic.Arithmetic.Power.binaryCircuit exponent).size

def Algebraic.Arithmetic.Power.binaryPowerCircuit {K : Type} [One K] (exponent : ℕ) : Circuit (signature K) 1 1

Binary powering under a name that is easy to mention at concrete exponents; its gate count is binaryPowerGateCount.

Equations

• Algebraic.Arithmetic.Power.binaryPowerCircuit exponent = Algebraic.Arithmetic.Power.binaryCircuit exponent

@[simp]

theorem Algebraic.Arithmetic.Power.size_binaryPowerCircuit {K : Type} [One K] (exponent : ℕ) : (binaryPowerCircuit exponent).size = binaryPowerGateCount exponent

The named binary-power circuit has binaryPowerGateCount gates.

def Algebraic.Arithmetic.Power.binaryMultiplicationCount (exponent : ℕ) : ℕ

Exact number of multiplication gates used by binaryCircuit.

Equations

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

@[simp]

theorem Algebraic.Arithmetic.Power.binaryCircuit_zero {K : Type} [One K] : binaryCircuit 0 = (Expression.constant 1).circuit

@[simp]

theorem Algebraic.Arithmetic.Power.binaryCircuit_one {K : Type} [One K] : binaryCircuit 1 = Circuit.id (signature K) 1

theorem Algebraic.Arithmetic.Power.binaryCircuit_bit {K : Type} [One K] (bit : Bool) (exponent : ℕ) (nonzero : exponent ≠ 0) : binaryCircuit (Nat.bit bit exponent) = if bit = true then multiplyInputCircuit (squareCircuit (binaryCircuit exponent)) else squareCircuit (binaryCircuit exponent)

@[simp]

theorem Algebraic.Arithmetic.Power.binaryMultiplicationCount_zero : binaryMultiplicationCount 0 = 0

@[simp]

theorem Algebraic.Arithmetic.Power.binaryMultiplicationCount_one : binaryMultiplicationCount 1 = 0

theorem Algebraic.Arithmetic.Power.binaryMultiplicationCount_bit (bit : Bool) (exponent : ℕ) (nonzero : exponent ≠ 0) : binaryMultiplicationCount (Nat.bit bit exponent) = binaryMultiplicationCount exponent + 1 + bit.toNat

theorem Algebraic.Arithmetic.Power.binaryCircuit_eval {K R : Type} [Semiring R] [One K] (constant : K → R) (mapsOne : constant 1 = 1) (input : Fin 1 → R) (exponent : ℕ) : (binaryCircuit exponent).eval (interpretation constant) input 0 = input 0 ^ exponent

Binary compilation computes the requested natural power.

@[simp]

theorem Algebraic.Arithmetic.Power.binaryPowerCircuit_eval {K R : Type} [Semiring R] [One K] (constant : K → R) (mapsOne : constant 1 = 1) (input : Fin 1 → R) (exponent : ℕ) : (binaryPowerCircuit exponent).eval (interpretation constant) input 0 = input 0 ^ exponent

The named binary-power circuit computes the requested natural power.

@[simp]

theorem Algebraic.Arithmetic.Power.binaryCircuit_multiplicationCost {K : Type} [One K] (exponent : ℕ) : (binaryCircuit exponent).cost multiplicationCost = binaryMultiplicationCount exponent

The multiplication cost of binary compilation is exactly the recursive binary count.

@[simp]

theorem Algebraic.Arithmetic.Power.binaryPowerCircuit_multiplicationCost {K : Type} [One K] (exponent : ℕ) : (binaryPowerCircuit exponent).cost multiplicationCost = binaryMultiplicationCount exponent

Multiplication cost of the named binary-power circuit.

@[simp]

theorem Algebraic.Arithmetic.Power.binaryCircuit_additionCost {K : Type} [One K] (exponent : ℕ) : (binaryCircuit exponent).cost additionCost = 0

Binary powering contains no addition gates.

@[simp]

theorem Algebraic.Arithmetic.Power.binaryPowerCircuit_additionCost {K : Type} [One K] (exponent : ℕ) : (binaryPowerCircuit exponent).cost additionCost = 0

The named binary-power circuit contains no addition gates.

theorem Algebraic.Arithmetic.Power.binaryMultiplicationCount_le_two_mul_log2 (exponent : ℕ) (positive : 0 < exponent) : binaryMultiplicationCount exponent ≤ 2 * exponent.log2

Binary powering uses at most twice the base-two logarithm many multiplications for every positive exponent.