Scatter, evaluate once per resource, and gather

One shared circuit sends each active incidence's suffix to its resource, evaluates the exact resource bank once, and returns the selected resource value to every incidence. Correctness requires only distinct active keys. The routing overhead is linear in incidences plus resources, and the bank cost is the sum over actual resource circuits, with no padding multiplier.

def Algebraic.MassProduction.Nonuniform.IncidenceEvaluation.routingCost (incidences resources keyWidth suffixWidth : ℕ) : ℕ

Common polynomial bound for both routing passes.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.IncidenceEvaluation.existsCircuit {resources incidences keyWidth inputs suffixWidth : ℕ} (valid : Fin incidences → Bool) (keys : Fin incidences → Fin keyWidth → DeMorgan.Wiring inputs) (suffixes : Fin incidences → Fin suffixWidth → DeMorgan.Wiring inputs) (resourceKeys : Fin resources → Fin keyWidth → Bool) (resourceKeysDistinct : Function.Injective resourceKeys) (members : Fin resources → Circuit DeMorgan.signature suffixWidth 1) : ∃ (evaluated : Circuit DeMorgan.signature inputs incidences), evaluated.cost DeMorgan.standardCost ≤ routingCost incidences resources keyWidth suffixWidth + ∑ resource : Fin resources, (members resource).cost DeMorgan.standardCost ∧ ∀ (input : Fin inputs → Bool) (incidence : Fin incidences) (resource : Fin resources), valid incidence = true → (fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys incidence bit)) = resourceKeys resource → (∀ (other : Fin incidences), valid other = true → ((fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys other bit)) = fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys incidence bit)) → other = incidence) → evaluated.eval DeMorgan.interpretation input incidence = (members resource).eval DeMorgan.interpretation (fun (bit : Fin suffixWidth) => DeMorgan.Wiring.eval input (suffixes incidence bit)) 0

Evaluate resources at the suffixes supplied by unique active incidences. All choices of circuits precede their runtime input.