Complete high-rate recovery from encoded request metadata

One circuit schedules arbitrary repeated targets, evaluates the exact resource bank, recovers each requested source bit, and restores the original request order. Copy, information-point, basis-bit, and suffix metadata are read from supplied wires. An offline prefix lookup can supply these wires.

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

Total overhead excluding the exact bank evaluation cost.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.ScheduledRecovery.existsCircuit {Source : Type u_1} {width dimension depth copies suffixWidth copyBits selectorBits payloadWidth inputs : ℕ} (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 : Source ↪ HighRate.InformationBit code copies) (function : Source → (Fin suffixWidth → Bool) → Bool) (copyFits : copies ≤ 2 ^ copyBits) (selectorFits : width ≤ 2 ^ selectorBits) (original : Fin (Sorting.networkRecords depth) → Fin payloadWidth → DeMorgan.Wiring inputs) (targetProjection : Fin (dimension * width) → Fin payloadWidth) (copyProjection : Fin copyBits → Fin payloadWidth) (selectorProjection : Fin selectorBits → Fin payloadWidth) (suffixProjection : Fin suffixWidth → Fin payloadWidth) (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 inputs (Sorting.networkRecords depth)), result.cost DeMorgan.standardCost ≤ overhead depth copies dimension width payloadWidth copyBits selectorBits suffixWidth + ∑ resource : Fin (HighRate.ResourceLayout.count copies dimension width), (members resource).cost DeMorgan.standardCost ∧ ∀ (input : Fin inputs → Bool) (sources : Fin (Sorting.networkRecords depth) → Source) (suffixes : Fin (Sorting.networkRecords depth) → Fin suffixWidth → Bool), (∀ (request : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)), DeMorgan.Wiring.eval input (original request (targetProjection bit)) = binaryExtensionVectorBits positive (↑(placement (sources request)).2.1) bit) → (∀ (request : Fin (Sorting.networkRecords depth)) (bit : Fin copyBits), DeMorgan.Wiring.eval input (original request (copyProjection bit)) = finiteIndexBits copyBits (placement (sources request)).1 bit) → (∀ (request : Fin (Sorting.networkRecords depth)) (bit : Fin selectorBits), DeMorgan.Wiring.eval input (original request (selectorProjection bit)) = finiteIndexBits selectorBits (placement (sources request)).2.2 bit) → (∀ (request : Fin (Sorting.networkRecords depth)) (bit : Fin suffixWidth), DeMorgan.Wiring.eval input (original request (suffixProjection bit)) = suffixes request bit) → ∀ (request : Fin (Sorting.networkRecords depth)), result.eval DeMorgan.interpretation input request = function (sources request) (suffixes request)

The complete scheduler/resource/recovery circuit computes every source request in its original order. There is no input-dependent circuit choice and no distinctness premise on the targets, prefixes, or suffixes.