Finite Uhlig theorem and sharpness predicates

This module packages the exact finite recursive construction used by Uhlig's theorem. It also states the denominator-free one-copy and mass-production sharpness predicates that form the asymptotic theorem's public interface.

Finite end-to-end theorem

theorem Algebraic.MassProduction.UhligTheorem.exists_finite_uhlig_circuit (prefixWidth baseWidth depth : ℕ) (base : ScalarSynthesis baseWidth) (baseBound : ℕ) (baseCost : ∀ (function : ScalarFunction Bool baseWidth), (base.circuit function).cost DeMorgan.standardCost ≤ baseBound) (function : ScalarFunction Bool (UhligRecursion.recursiveWidth prefixWidth baseWidth depth)) (copies : ℕ) (copiesPositive : 0 < copies) (copiesBound : copies ≤ 2 ^ depth) : ∃ (circuit : Circuit DeMorgan.signature (copies * UhligRecursion.recursiveWidth prefixWidth baseWidth depth) copies), circuit.ComputesWith DeMorgan.interpretation (directProduct function copies) ∧ circuit.cost DeMorgan.standardCost ≤ UhligRecursion.resourceCount prefixWidth ^ depth * (baseBound + depth * UhligRecursion.layerOverheadEnvelope prefixWidth (UhligRecursion.recursiveWidth prefixWidth baseWidth depth))

Exact finite Uhlig construction for every positive sub-batch of the power-of-two batch produced by the recursion.

theorem Algebraic.MassProduction.UhligTheorem.exists_finite_uhlig_circuit_at_width (prefixWidth baseWidth depth inputs : ℕ) (widthIdentity : UhligRecursion.recursiveWidth prefixWidth baseWidth depth = inputs) (base : ScalarSynthesis baseWidth) (baseBound : ℕ) (baseCost : ∀ (function : ScalarFunction Bool baseWidth), (base.circuit function).cost DeMorgan.standardCost ≤ baseBound) (function : ScalarFunction Bool inputs) (copies : ℕ) (copiesPositive : 0 < copies) (copiesBound : copies ≤ 2 ^ depth) : ∃ (circuit : Circuit DeMorgan.signature (copies * inputs) copies), circuit.ComputesWith DeMorgan.interpretation (directProduct function copies) ∧ circuit.cost DeMorgan.standardCost ≤ UhligRecursion.resourceCount prefixWidth ^ depth * (baseBound + depth * UhligRecursion.layerOverheadEnvelope prefixWidth inputs)

Width-transported form of the finite construction.

def Algebraic.MassProduction.UhligTheorem.HasSharpOneCopyCost (family : ScalarSynthesisFamily) : Prop

Denominator-free formulation of a sharp one-copy upper bound. For every positive integer precision q, the normalized coefficient is eventually at most (q + 1) / q.

Equations

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

def Algebraic.MassProduction.UhligTheorem.normalizedBaseBound (precision width : ℕ) : ℕ

Uniform integral bound extracted from one normalized sharp estimate.

Equations

• Algebraic.MassProduction.UhligTheorem.normalizedBaseBound precision width = (precision + 1) * 2 ^ width / (precision * width)

theorem Algebraic.MassProduction.UhligTheorem.normalizedBaseBound_spec (precision width : ℕ) : precision * normalizedBaseBound precision width * width ≤ (precision + 1) * 2 ^ width

theorem Algebraic.MassProduction.UhligTheorem.circuit_cost_le_normalizedBaseBound (family : ScalarSynthesisFamily) (precision width : ℕ) (precisionPositive : 0 < precision) (widthPositive : 0 < width) (function : ScalarFunction Bool width) (sharpBound : precision * ((family width).circuit function).cost DeMorgan.standardCost * width ≤ (precision + 1) * 2 ^ width) : ((family width).circuit function).cost DeMorgan.standardCost ≤ normalizedBaseBound precision width

def Algebraic.MassProduction.UhligTheorem.IsUhligDepth (depth : ℕ → ℕ) : Prop

Exact discrete reading of depth(n) = o(n / log n). Quantifying over every fixed positive multiplier avoids division and real-valued side conditions.

Equations

• Algebraic.MassProduction.UhligTheorem.IsUhligDepth depth = ∀ (multiplier : ℕ), 0 < multiplier → ∀ᶠ (inputs : ℕ) in Filter.atTop, multiplier * depth inputs * Nat.log 2 inputs ≤ inputs

def Algebraic.MassProduction.UhligTheorem.HasSharpMassProduction (depth : ℕ → ℕ) : Prop

Sharp mass production through the copy budget 2 ^ depth(n), stated directly for minimum De Morgan cost.

Equations

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