Recursive Uhlig circuit

This module iterates the exact finite two-copy layer. Scalar synthesis data is passed explicitly, so the construction introduces no instance-search burden. It proves semantic correctness and exact cost identities for the recursion.

@[reducible]

def Algebraic.MassProduction.UhligRecursion.recursiveWidth (prefixWidth baseWidth : ℕ) : ℕ → ℕ

Width left after depth equal prefix blocks have been restored.

Equations

• Algebraic.MassProduction.UhligRecursion.recursiveWidth prefixWidth baseWidth 0 = baseWidth
• Algebraic.MassProduction.UhligRecursion.recursiveWidth prefixWidth baseWidth depth.succ = prefixWidth + Algebraic.MassProduction.UhligRecursion.recursiveWidth prefixWidth baseWidth depth

@[reducible]

def Algebraic.MassProduction.UhligRecursion.recursiveCopies : ℕ → ℕ

Number of copies after depth two-copy layers.

Equations

• Algebraic.MassProduction.UhligRecursion.recursiveCopies 0 = 1
• Algebraic.MassProduction.UhligRecursion.recursiveCopies depth.succ = 2 * Algebraic.MassProduction.UhligRecursion.recursiveCopies depth

theorem Algebraic.MassProduction.UhligRecursion.recursiveCopies_eq_two_pow (depth : ℕ) : recursiveCopies depth = 2 ^ depth

theorem Algebraic.MassProduction.UhligRecursion.recursiveWidth_eq (prefixWidth baseWidth depth : ℕ) : recursiveWidth prefixWidth baseWidth depth = depth * prefixWidth + baseWidth

noncomputable def Algebraic.MassProduction.UhligRecursion.recursiveGateCount (prefixWidth baseWidth : ℕ) (base : ScalarSynthesis baseWidth) (depth : ℕ) : ScalarFunction Bool (recursiveWidth prefixWidth baseWidth depth) → ℕ

Gate count determined by the chosen base synthesis and every explicit routing/decoding layer above it.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.UhligRecursion.recursiveGateCount prefixWidth baseWidth base 0 function = 1 * base.gateCount function

noncomputable def Algebraic.MassProduction.UhligRecursion.recursiveCircuit (prefixWidth baseWidth : ℕ) (base : ScalarSynthesis baseWidth) (depth : ℕ) (function : ScalarFunction Bool (recursiveWidth prefixWidth baseWidth depth)) : Circuit DeMorgan.signature (recursiveCopies depth * recursiveWidth prefixWidth baseWidth depth) (recursiveCopies depth)

The recursive circuit obtained by using the supplied synthesis at the base and one exact Uhlig layer per recursive step.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.UhligRecursion.recursiveCircuit prefixWidth baseWidth base 0 function = (base.circuit function).replicateScalar 1

@[simp]

theorem Algebraic.MassProduction.UhligRecursion.recursiveCircuit_size (prefixWidth baseWidth : ℕ) (base : ScalarSynthesis baseWidth) (depth : ℕ) (function : ScalarFunction Bool (recursiveWidth prefixWidth baseWidth depth)) : (recursiveCircuit prefixWidth baseWidth base depth function).size = recursiveGateCount prefixWidth baseWidth base depth function

The recursive circuit emits exactly recursiveGateCount gates.

theorem Algebraic.MassProduction.UhligRecursion.recursiveCircuit_computes (prefixWidth baseWidth : ℕ) (base : ScalarSynthesis baseWidth) (depth : ℕ) (function : ScalarFunction Bool (recursiveWidth prefixWidth baseWidth depth)) : (recursiveCircuit prefixWidth baseWidth base depth function).ComputesWith DeMorgan.interpretation (directProduct function (recursiveCopies depth))

Iterating the finite layer computes exactly 2 ^ depth independent copies of the original function.

@[simp]

theorem Algebraic.MassProduction.UhligRecursion.recursiveCircuit_cost_zero (prefixWidth baseWidth : ℕ) (base : ScalarSynthesis baseWidth) (function : ScalarFunction Bool baseWidth) : (recursiveCircuit prefixWidth baseWidth base 0 function).cost DeMorgan.standardCost = (base.circuit function).cost DeMorgan.standardCost

@[simp]

theorem Algebraic.MassProduction.UhligRecursion.recursiveCircuit_cost_succ (prefixWidth baseWidth : ℕ) (base : ScalarSynthesis baseWidth) (depth : ℕ) (function : ScalarFunction Bool (recursiveWidth prefixWidth baseWidth (depth + 1))) : (recursiveCircuit prefixWidth baseWidth base (depth + 1) function).cost DeMorgan.standardCost = ∑ resource : Fin (UhligCircuit.prefixLast prefixWidth + 2), (∑ _pair : Fin (recursiveCopies depth), (UhligCircuit.resourceRouterCircuit resource).cost DeMorgan.standardCost + (recursiveCircuit prefixWidth baseWidth base depth (UhligCircuit.resourceFunction function resource)).cost DeMorgan.standardCost) + ∑ output : Fin (2 * recursiveCopies depth), have pairSide := UhligCircuit.decoderPairSide output; (UhligCircuit.sharedDecodedCircuit pairSide.1 pairSide.2).cost DeMorgan.standardCost

Exact recursive cost identity. The first summand at each resource is explicit routing overhead, and the second is the recursively shared resource computation.