Complete nonuniform mass-production circuit on raw request inputs

The shared prefix table supplies the code placement metadata, while fixed wiring retains each suffix. The scheduler and resource pipeline then compute the direct product of the requested Boolean function. The finite bound includes every runtime stage and the exact sum of resource-circuit costs.

def Algebraic.MassProduction.Nonuniform.RuntimeComposition.overhead (depth copies prefixWidth dimension width suffixWidth copyBits selectorBits : ℕ) : ℕ

Complete runtime overhead apart from the actual resource evaluations.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.RuntimeComposition.existsCircuit {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) (members : Fin (HighRate.ResourceLayout.count copies dimension width) → Circuit DeMorgan.signature suffixWidth 1) (membersCorrect : ∀ (resource : Fin (HighRate.ResourceLayout.count copies dimension width)) (suffix : Fin suffixWidth → Bool), (members resource).eval DeMorgan.interpretation suffix 0 = HighRate.ResourceLayout.function positive code placement function resource suffix) : ∃ (result : Circuit DeMorgan.signature (Sorting.networkRecords depth * (prefixWidth + suffixWidth)) (Sorting.networkRecords depth)), result.cost DeMorgan.standardCost ≤ overhead depth copies prefixWidth dimension width suffixWidth copyBits selectorBits + ∑ resource : Fin (HighRate.ResourceLayout.count copies dimension width), (members resource).cost DeMorgan.standardCost ∧ result.ComputesWith DeMorgan.interpretation (directProduct (RuntimePipeline.requestFunction function) (Sorting.networkRecords depth))

One circuit computes all raw prefix/suffix requests, including repeated requests, with no unproved scheduler, encoding, or routing premise.

theorem Algebraic.MassProduction.Nonuniform.RuntimeComposition.booleanMassComplexity_le {width dimension depth prefixWidth copies suffixWidth copyBits selectorBits resourceBound : ℕ} (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) (members : Fin (HighRate.ResourceLayout.count copies dimension width) → Circuit DeMorgan.signature suffixWidth 1) (membersCorrect : ∀ (resource : Fin (HighRate.ResourceLayout.count copies dimension width)) (suffix : Fin suffixWidth → Bool), (members resource).eval DeMorgan.interpretation suffix 0 = HighRate.ResourceLayout.function positive code placement function resource suffix) (memberBound : ∀ (resource : Fin (HighRate.ResourceLayout.count copies dimension width)), (members resource).cost DeMorgan.standardCost ≤ resourceBound) : booleanMassComplexity (RuntimePipeline.requestFunction function) (Sorting.networkRecords depth) ≤ ↑(overhead depth copies prefixWidth dimension width suffixWidth copyBits selectorBits + HighRate.ResourceLayout.count copies dimension width * resourceBound)

The concrete runtime construction bounds Boolean mass complexity by its full overhead plus one evaluation of every actual resource function.