A compact shared-router size bound

The two sorting passes and shared propagation scan cost a linear number of records times a fixed polynomial in key width, value width, and sorting depth.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.routingCircuit_cost_le_polynomial {depth keyWidth valueWidth : ℕ} : (routingCircuit depth keyWidth (depth + 1) valueWidth).cost DeMorgan.standardCost ≤ 128 * Sorting.networkRecords depth * (depth + keyWidth + valueWidth + 2) ^ 5

A compact polynomial bound retaining linear dependence on record count.