Shared XOR folds over fixed valid slots

Each request folds its returned point values once. Invalid slots are wired to false. Compiling arithmetic addition preserves sharing and charges four De Morgan gates per scalar slot, avoiding formula duplication.

noncomputable def Algebraic.MassProduction.Nonuniform.MaskedXor.circuit {slots : ℕ} (valid : Fin slots → Bool) (requests : ℕ) : Circuit DeMorgan.signature (requests * slots) requests

One masked XOR fold for each request's point list.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MaskedXor.circuit_size {slots : ℕ} (valid : Fin slots → Bool) (requests : ℕ) : (circuit valid requests).size = requests * ({slot : Fin slots | valid slot = false}.card + UhligCircuit.xorInputGateCount slots)

The exact gate count of circuit: each request's fold has one constant gate for every invalid slot, which is wired to false, plus the UhligCircuit.xorInputGateCount slots gates of the XOR fold; valid slots are free input wires.

theorem Algebraic.MassProduction.Nonuniform.MaskedXor.circuit_eval {slots requests : ℕ} (valid : Fin slots → Bool) (input : Fin (requests * slots) → Bool) (request : Fin requests) : (circuit valid requests).eval DeMorgan.interpretation input request = ∑ slot : Fin slots, if valid slot = true then input (finProdFinEquiv (request, slot)) else false

Each output is the Boolean sum over that request's valid point slots.

theorem Algebraic.MassProduction.Nonuniform.MaskedXor.circuit_cost {slots : ℕ} (valid : Fin slots → Bool) (requests : ℕ) : (circuit valid requests).cost DeMorgan.standardCost = requests * slots * 4

Exactly four charged gates per padded scalar slot.