Complete finite bound with synthesized resource functions

Use the already-proved coefficient-one Lupanov synthesis for every shorter Boolean resource function. This discharges resource-circuit existence and correctness; the remaining finite hypotheses describe only the chosen code, its source-bit placement, index widths, and the geometric direction budget.

def Algebraic.MassProduction.Nonuniform.LupanovRuntime.resourceCost (suffixWidth : ℕ) : ℕ

Explicit finite cost bound for one shorter Boolean resource function.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.LupanovRuntime.normalizedResourceBound (precision : ℕ) (precisionPositive : 0 < precision) : ∃ (cutoff : ℕ), ∀ (suffixWidth : ℕ), cutoff ≤ suffixWidth → ∀ (function : ScalarFunction Bool suffixWidth), (LupanovSynthesis.lupanovCircuit suffixWidth function).cost DeMorgan.standardCost ≤ (precision + 1) * 2 ^ suffixWidth / (precision * suffixWidth)

Sharp one-copy synthesis supplies an eventual integral resource-cost bound, uniformly over every Boolean function of the shorter suffix.

theorem Algebraic.MassProduction.Nonuniform.LupanovRuntime.booleanMassComplexity_le_of_resourceBound {width dimension depth prefixWidth copies suffixWidth copyBits selectorBits bound : ℕ} (positive : 0 < width) (dimensionPositive : 0 < dimension) (budget : 512 * Sorting.networkRecords depth * Nat.card (BinaryExtension width) ≤ Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (code : HighRate.LineCode (BinaryExtension width) (Fin dimension)) (placement : Fin (2 ^ prefixWidth) ↪ HighRate.InformationBit code copies) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (copyFits : copies ≤ 2 ^ copyBits) (selectorFits : width ≤ 2 ^ selectorBits) (bounded : ∀ (resourceFunction : ScalarFunction Bool suffixWidth), (LupanovSynthesis.lupanovCircuit suffixWidth resourceFunction).cost DeMorgan.standardCost ≤ bound) : booleanMassComplexity (RuntimePipeline.requestFunction function) (Sorting.networkRecords depth) ≤ ↑(RuntimeComposition.overhead depth copies prefixWidth dimension width suffixWidth copyBits selectorBits + HighRate.ResourceLayout.count copies dimension width * bound)

Any uniform bound on the actual Lupanov resource circuits can replace the explicit finite envelope in the complete runtime construction.

theorem Algebraic.MassProduction.Nonuniform.LupanovRuntime.booleanMassComplexity_le {width dimension depth prefixWidth copies suffixWidth copyBits selectorBits : ℕ} (positive : 0 < width) (dimensionPositive : 0 < dimension) (budget : 512 * Sorting.networkRecords depth * Nat.card (BinaryExtension width) ≤ Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (code : HighRate.LineCode (BinaryExtension width) (Fin dimension)) (placement : Fin (2 ^ prefixWidth) ↪ HighRate.InformationBit code copies) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (copyFits : copies ≤ 2 ^ copyBits) (selectorFits : width ≤ 2 ^ selectorBits) : booleanMassComplexity (RuntimePipeline.requestFunction function) (Sorting.networkRecords depth) ≤ ↑(RuntimeComposition.overhead depth copies prefixWidth dimension width suffixWidth copyBits selectorBits + HighRate.ResourceLayout.count copies dimension width * resourceCost suffixWidth)

Concrete high-rate mass-production bound with every resource function synthesized, rather than supplied as an additional circuit premise.