Shared scatter from distinct active incidences

Fixed invalid slots contribute false through free wiring. Batched OR then routes an active incidence's entire payload to its resource, provided no other active incidence has the same key. Empty resources may receive false.

def Algebraic.MassProduction.Nonuniform.MaskedScatter.values {sources valueWidth inputs : ℕ} (valid : Fin sources → Bool) (payload : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (source : Fin sources) (bit : Fin valueWidth) : DeMorgan.Wiring inputs

Invalid slots contribute zero without any charged masking gates.

Equations

• Algebraic.MassProduction.Nonuniform.MaskedScatter.values valid payload source bit = if valid source = true then payload source bit else Algebraic.DeMorgan.Wiring.constant false

theorem Algebraic.MassProduction.Nonuniform.MaskedScatter.values_eval_iff {sources valueWidth inputs : ℕ} (valid : Fin sources → Bool) (payload : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (source : Fin sources) (bit : Fin valueWidth) : DeMorgan.Wiring.eval input (values valid payload source bit) = true ↔ valid source = true ∧ DeMorgan.Wiring.eval input (payload source bit) = true

An active source is the only way a masked payload bit can be true.

theorem Algebraic.MassProduction.Nonuniform.MaskedScatter.existsCircuit {sources keyWidth inputs valueWidth resources : ℕ} (valid : Fin sources → Bool) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (payload : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (resourceKeys : Fin resources → Fin keyWidth → Bool) : ∃ (scattered : Circuit DeMorgan.signature inputs (resources * valueWidth)), scattered.cost DeMorgan.standardCost ≤ 256 * (sources + resources + 1) * (FiniteParameters.binaryDepth (sources + resources + 1) + keyWidth + valueWidth + 2) ^ 5 ∧ ∀ (input : Fin inputs → Bool) (source : Fin sources) (resource : Fin resources), valid source = true → (fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source bit)) = resourceKeys resource → (∀ (other : Fin sources), valid other = true → ((fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys other bit)) = fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source bit)) → other = source) → ∀ (bit : Fin valueWidth), scattered.eval DeMorgan.interpretation input (finProdFinEquiv (resource, bit)) = DeMorgan.Wiring.eval input (payload source bit)

A fixed shared scatter circuit routes every unique active source's payload to its matching resource. The bound counts all sources and resources once, regardless of how many payload bits are returned.