Documentation

Complexitylib.Algebraic.MassProduction.LupanovSynthesis

Sharp Lupanov synthesis #

This module packages the finite circuit and parameter bounds into a uniform coefficient-one synthesis family, then feeds that explicit family into the sharp Uhlig theorem.

All synthesis data is passed explicitly. In particular, this module adds no type-class instances.

The coefficient-one synthesis family #

source
noncomputable def Algebraic.MassProduction.LupanovSynthesis.lupanovCircuit (inputs : ℕ) (function : ScalarFunction Bool inputs) :
Circuit DeMorgan.signature inputs 1

Uniform width-indexed form of the finite Lupanov circuit.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.MassProduction.LupanovSynthesis.lupanovCircuit_size (inputs : ℕ) (function : ScalarFunction Bool inputs) :
    (lupanovCircuit inputs function).size = synthesisGateCount (ShannonSynthesis.reindexFunction ⋯ function) (lupanovBlockSize inputs)
    source
    @[simp]
    theorem Algebraic.MassProduction.LupanovSynthesis.lupanovCircuit_eval (inputs : ℕ) (function : ScalarFunction Bool inputs) (input : Fin inputs → Bool) :
    (lupanovCircuit inputs function).eval DeMorgan.interpretation input 0 = function input
    source
    theorem Algebraic.MassProduction.LupanovSynthesis.lupanovCircuit_computes (inputs : ℕ) (function : ScalarFunction Bool inputs) :
    (lupanovCircuit inputs function).ComputesWith DeMorgan.interpretation (scalarTarget function)
    source
    theorem Algebraic.MassProduction.LupanovSynthesis.lupanovCircuit_cost_le (inputs : ℕ) (function : ScalarFunction Bool inputs) :
    (lupanovCircuit inputs function).cost DeMorgan.standardCost ≤ costBound (lupanovAddressWidth inputs) (lupanovDataWidth inputs) (lupanovBlockSize inputs)
    source
    noncomputable def Algebraic.MassProduction.LupanovSynthesis.lupanovScalarSynthesis (inputs : ℕ) :
    ScalarSynthesis inputs

    Explicit one-copy synthesis data at every width.

    Equations
    Instances For
      source
      noncomputable def Algebraic.MassProduction.LupanovSynthesis.lupanovFamily :
      ScalarSynthesisFamily

      The Lupanov family as explicit dependent data, not a typeclass.

      Equations
      Instances For
        source
        @[simp]
        theorem Algebraic.MassProduction.LupanovSynthesis.lupanovFamily_circuit (inputs : ℕ) (function : ScalarFunction Bool inputs) :
        (lupanovFamily inputs).circuit function = lupanovCircuit inputs function
        source
        theorem Algebraic.MassProduction.LupanovSynthesis.lupanovFamily_hasSharpOneCopyCost :
        UhligTheorem.HasSharpOneCopyCost lupanovFamily

        Lupanov's coefficient-one one-copy upper bound, in the exact integral form consumed by the Uhlig recursion.

        The following is the unconditional sharp Uhlig theorem. It combines the coefficient-one Lupanov family above with the exact recursive two-copy circuit from UhligRecursion. Its discrete IsUhligDepth premise is precisely the denominator-free form of depth(n) = o(n / log n), so it covers every batch size 1 <= t <= 2 ^ depth(n) with asymptotic leading coefficient one.

        source
        theorem Algebraic.MassProduction.LupanovSynthesis.uhlig_massProduction (depth : ℕ → ℕ) (depthSmall : UhligTheorem.IsUhligDepth depth) :
        UhligTheorem.HasSharpMassProduction depth