Batched lookup with canonical padding and a compact size bound

For T = 2^keyWidth + requests, the next-power-of-two layout contains fewer than 2*T records. The complete lookup circuit has at most 256*T*(ceil(log2 T) + keyWidth + valueWidth + 2)^5 charged gates.

theorem Algebraic.MassProduction.Nonuniform.BatchLookup.circuit_cost_le_polynomial {keyWidth valueWidth requests padding depth : ℕ} (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) : (circuit table recordCount).cost DeMorgan.standardCost ≤ 128 * Sorting.networkRecords depth * (depth + keyWidth + valueWidth + 2) ^ 5

A compact polynomial bound retaining linear dependence on record count.

theorem Algebraic.MassProduction.Nonuniform.BatchLookup.existsCircuit (keyWidth valueWidth requests : ℕ) (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) : ∃ (lookup : Circuit DeMorgan.signature (requests * keyWidth) (requests * valueWidth)), (∀ (input : Fin (requests * keyWidth) → Bool) (request : Fin requests) (bit : Fin valueWidth), lookup.eval DeMorgan.interpretation input (finProdFinEquiv (request, bit)) = table (fun (addressBit : Fin keyWidth) => input (finProdFinEquiv (request, addressBit))) bit) ∧ lookup.cost DeMorgan.standardCost ≤ 256 * (2 ^ keyWidth + requests) * (FiniteParameters.binaryDepth (2 ^ keyWidth + requests) + keyWidth + valueWidth + 2) ^ 5

The concrete lookup bound holds for every table and every query count, using canonical padding. Constants in the source table are hardwired.