Quantitative bounds for recursive Uhlig mass production

Building on the exact recursive circuit, this module bounds the resource tree and accumulated routing/decoding overhead. Every estimate is an explicit natural-number inequality used by the finite and asymptotic Uhlig theorems.

def Algebraic.MassProduction.UhligRecursion.resourceCount (prefixWidth : ℕ) : ℕ

Number of shorter resource functions created by one Uhlig layer.

Equations

• Algebraic.MassProduction.UhligRecursion.resourceCount prefixWidth = Algebraic.MassProduction.UhligCircuit.prefixLast prefixWidth + 2

theorem Algebraic.MassProduction.UhligRecursion.resourceCount_eq (prefixWidth : ℕ) : resourceCount prefixWidth = 2 ^ prefixWidth + 1

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

Total nonrecursive overhead accumulated by the full resource tree.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.UhligRecursion.recursiveOverhead prefixWidth baseWidth 0 = 0

def Algebraic.MassProduction.UhligRecursion.layerOverheadEnvelope (prefixWidth suffixWidth : ℕ) : ℕ

The overhead of one layer after factoring out its number of request pairs. Keeping this as an explicit natural-number expression makes the subsequent recurrence bounds independent of asymptotic notation.

Equations

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

theorem Algebraic.MassProduction.UhligRecursion.sharedLayerOverheadBound_eq (prefixWidth suffixWidth pairs : ℕ) : UhligCircuit.sharedLayerOverheadBound prefixWidth suffixWidth pairs = pairs * layerOverheadEnvelope prefixWidth suffixWidth

theorem Algebraic.MassProduction.UhligRecursion.layerOverheadEnvelope_mono_suffix (prefixWidth small large : ℕ) (bounded : small ≤ large) : layerOverheadEnvelope prefixWidth small ≤ layerOverheadEnvelope prefixWidth large

theorem Algebraic.MassProduction.UhligRecursion.resourceCount_positive (prefixWidth : ℕ) : 0 < resourceCount prefixWidth

theorem Algebraic.MassProduction.UhligRecursion.recursiveCopies_le_resourcePower (prefixWidth depth : ℕ) : recursiveCopies depth ≤ resourceCount prefixWidth ^ depth

theorem Algebraic.MassProduction.UhligRecursion.sub_mul_succ_pow_le_pow_succ (base depth : ℕ) (depthLe : depth ≤ base) : (base - depth) * (base + 1) ^ depth ≤ base ^ (depth + 1)

A denominator-free upper estimate for (base + 1)^depth. It is the finite inequality behind the fact that the extra one resource per layer does not alter Uhlig's leading coefficient when depth / base tends to zero.

theorem Algebraic.MassProduction.UhligRecursion.precision_mul_resourcePower_le (precision prefixWidth depth : ℕ) (depthSmall : (precision + 1) * depth ≤ 2 ^ prefixWidth) : precision * resourceCount prefixWidth ^ depth ≤ (precision + 1) * (2 ^ prefixWidth) ^ depth

Quantitative leading-coefficient control for the resource tree. If the base resource count 2^p dominates (precision + 1) * depth, then the extra resource at each layer costs at most the factor (precision + 1) / precision.

theorem Algebraic.MassProduction.UhligRecursion.recursiveOverhead_le (prefixWidth baseWidth depth maxWidth : ℕ) (widthBound : recursiveWidth prefixWidth baseWidth depth ≤ maxWidth) : recursiveOverhead prefixWidth baseWidth depth ≤ depth * resourceCount prefixWidth ^ depth * layerOverheadEnvelope prefixWidth maxWidth

Closed finite bound for all routing and decoding accumulated through the resource tree. The chosen maxWidth may be any upper bound on the final recursive width; in applications it is the original input width.

theorem Algebraic.MassProduction.UhligRecursion.recursiveCircuit_cost_le (prefixWidth baseWidth : ℕ) (base : ScalarSynthesis baseWidth) (baseBound : ℕ) (baseCost : ∀ (function : ScalarFunction Bool baseWidth), (base.circuit function).cost DeMorgan.standardCost ≤ baseBound) (depth : ℕ) (function : ScalarFunction Bool (recursiveWidth prefixWidth baseWidth depth)) : (recursiveCircuit prefixWidth baseWidth base depth function).cost DeMorgan.standardCost ≤ resourceCount prefixWidth ^ depth * baseBound + recursiveOverhead prefixWidth baseWidth depth

Finite quantitative Uhlig recurrence. A uniform scalar base bound B lifts to (2^p + 1)^d * B plus the fully explicit routing/decoding overhead.

theorem Algebraic.MassProduction.UhligRecursion.recursiveCircuit_cost_le_closed (prefixWidth baseWidth : ℕ) (base : ScalarSynthesis baseWidth) (baseBound : ℕ) (baseCost : ∀ (function : ScalarFunction Bool baseWidth), (base.circuit function).cost DeMorgan.standardCost ≤ baseBound) (depth maxWidth : ℕ) (widthBound : recursiveWidth prefixWidth baseWidth depth ≤ maxWidth) (function : ScalarFunction Bool (recursiveWidth prefixWidth baseWidth depth)) : (recursiveCircuit prefixWidth baseWidth base depth function).cost DeMorgan.standardCost ≤ resourceCount prefixWidth ^ depth * (baseBound + depth * layerOverheadEnvelope prefixWidth maxWidth)

The recursive cost recurrence with the accumulated overhead replaced by its closed envelope bound.