Asymptotic bounds for Uhlig mass production

This module separates the two quantitative estimates used by the sharp theorem: finite control of the recursive leading term and eventual negligibility of the explicit routing and decoding overhead.

Finite leading-term arithmetic

theorem Algebraic.MassProduction.UhligTheorem.recursiveWidth_uhligBaseWidth (depth inputs : ℕ) (blocksFit : depth * uhligPrefixWidth inputs ≤ inputs) : UhligRecursion.recursiveWidth (uhligPrefixWidth inputs) (uhligBaseWidth depth inputs) depth = inputs

theorem Algebraic.MassProduction.UhligTheorem.precision_cube_mul_mainTerm_le (precision prefixWidth baseWidth depth baseBound : ℕ) (baseSharp : precision * baseBound * baseWidth ≤ (precision + 1) * 2 ^ baseWidth) (resourceSmall : (precision + 1) * depth ≤ 2 ^ prefixWidth) (removedWidthSmall : precision * depth * prefixWidth ≤ baseWidth) : precision ^ 3 * (UhligRecursion.resourceCount prefixWidth ^ depth * baseBound) * (depth * prefixWidth + baseWidth) ≤ (precision + 1) ^ 3 * 2 ^ (depth * prefixWidth + baseWidth)

Three coefficient losses are kept separate: the terminal sharp synthesis, the extra resource per layer, and replacing the terminal width in the denominator by the full width.

def Algebraic.MassProduction.UhligTheorem.internalPrecision (precision : ℕ) : ℕ

A convenient internal precision large enough to allocate half of the final coefficient slack to the main term.

Equations

• Algebraic.MassProduction.UhligTheorem.internalPrecision precision = 16 * (precision + 1)

theorem Algebraic.MassProduction.UhligTheorem.internalPrecision_positive (precision : ℕ) : 0 < internalPrecision precision

theorem Algebraic.MassProduction.UhligTheorem.twice_mul_succ_cube_le (precision : ℕ) : 2 * precision * (internalPrecision precision + 1) ^ 3 ≤ (2 * precision + 1) * internalPrecision precision ^ 3

theorem Algebraic.MassProduction.UhligTheorem.mainTerm_with_allocated_slack (precision mainTerm inputs : ℕ) (normalized : internalPrecision precision ^ 3 * mainTerm * inputs ≤ (internalPrecision precision + 1) ^ 3 * 2 ^ inputs) : 2 * precision * mainTerm * inputs ≤ (2 * precision + 1) * 2 ^ inputs

theorem Algebraic.MassProduction.UhligTheorem.combine_main_and_overhead (precision cost mainTerm overhead inputs : ℕ) (costBound : cost ≤ mainTerm + overhead) (mainBound : 2 * precision * mainTerm * inputs ≤ (2 * precision + 1) * 2 ^ inputs) (overheadBound : 2 * precision * inputs * overhead ≤ 2 ^ inputs) : precision * cost * inputs ≤ (precision + 1) * 2 ^ inputs

Negligibility of the explicit overhead

theorem Algebraic.MassProduction.UhligTheorem.resourcePower_le_two_mul (prefixWidth depth : ℕ) (depthSmall : 2 * depth ≤ 2 ^ prefixWidth) : UhligRecursion.resourceCount prefixWidth ^ depth ≤ 2 * (2 ^ prefixWidth) ^ depth

theorem Algebraic.MassProduction.UhligTheorem.normalized_overhead_le_of_growth (precision inputs depth : ℕ) (inputsLarge : 2 ≤ inputs) (depthLe : depth ≤ inputs) (resourceSmall : 2 * depth ≤ 2 ^ uhligPrefixWidth inputs) (removedExponentSmall : uhligPrefixWidth inputs * depth ≤ inputs / 2) (polynomialAbsorbed : 256 * precision * inputs ^ 10 ≤ 2 ^ (inputs / 2)) : 2 * precision * inputs * (UhligRecursion.resourceCount (uhligPrefixWidth inputs) ^ depth * (depth * UhligRecursion.layerOverheadEnvelope (uhligPrefixWidth inputs) inputs)) ≤ 2 ^ inputs

theorem Algebraic.MassProduction.UhligTheorem.eventually_normalized_overhead_le (depth : ℕ → ℕ) (depthSmall : IsUhligDepth depth) (precision : ℕ) : ∀ᶠ (inputs : ℕ) in Filter.atTop, 2 * precision * inputs * (UhligRecursion.resourceCount (uhligPrefixWidth inputs) ^ depth inputs * (depth inputs * UhligRecursion.layerOverheadEnvelope (uhligPrefixWidth inputs) inputs)) ≤ 2 ^ inputs

For every fixed coefficient precision, the complete explicit routing and decoding overhead is eventually smaller than the reserved half-unit of coefficient slack.