Uhlig's sharp mass-production theorem

This module turns the exact two-copy recursion into the classical 2 ^ o(n / log n) statement. The asymptotic hypothesis is expressed by ordinary natural-number inequalities, and synthesis data is passed explicitly rather than through typeclass instances.

The finite recursive theorem and its asymptotic estimates live in focused supporting modules. This module assembles them into the sharp theorem, parameterized by a sharp one-copy synthesis family. The separate Lupanov module discharges that premise.

Conditional sharp Uhlig theorem

theorem Algebraic.MassProduction.UhligTheorem.uhlig_of_sharp_one_copy (family : ScalarSynthesisFamily) (oneCopySharp : HasSharpOneCopyCost family) (depth : ℕ → ℕ) (depthSmall : IsUhligDepth depth) : HasSharpMassProduction depth

Uhlig's theorem, reduced exactly to sharp one-copy synthesis. Any explicit synthesis family with normalized coefficient one remains sharp for every copy budget 2 ^ depth(n) with depth(n) * log_2(n) = o(n).