Shared gather from an exact resource bank

Each fixed resource key labels one evaluated Boolean value. Dynamic queries, including repeated queries, recover that value in query order. Routing padding does not create additional resource evaluations.

theorem Algebraic.MassProduction.Nonuniform.ResourceGather.existsCircuit {resources keyWidth inputs queries : ℕ} (resourceKeys : Fin resources → Fin keyWidth → Bool) (distinct : Function.Injective resourceKeys) (values : Fin resources → DeMorgan.Wiring inputs) (queryKeys : Fin queries → Fin keyWidth → DeMorgan.Wiring inputs) : ∃ (gathered : Circuit DeMorgan.signature inputs queries), gathered.cost DeMorgan.standardCost ≤ 256 * (resources + queries + 1) * (FiniteParameters.binaryDepth (resources + queries + 1) + keyWidth + 1 + 2) ^ 5 ∧ ∀ (input : Fin inputs → Bool) (query : Fin queries) (resource : Fin resources), (fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (queryKeys query bit)) = resourceKeys resource → gathered.eval DeMorgan.interpretation input query = DeMorgan.Wiring.eval input (values resource)

Gather the resource selected by each dynamic query.