Aggregating point conflicts into clean requests

A request is clean when none of its point slots has a conflict. The shared point-conflict circuit runs once; each request adds one OR per slot and one negation. Slot counts may be zero, in which case every request is clean.

def Algebraic.MassProduction.Nonuniform.GroupClean.expression {slots pointCount : ℕ} (points : Fin slots → Fin pointCount) : DeMorgan.Expression pointCount

A clean request is the negation of the OR of all its point conflicts.

Equations

• Algebraic.MassProduction.Nonuniform.GroupClean.expression points = (Algebraic.DeMorgan.Expression.finOr slots fun (slot : Fin slots) => Algebraic.DeMorgan.Expression.input (points slot)).not

def Algebraic.MassProduction.Nonuniform.GroupClean.flagsCircuit {requests slots pointCount : ℕ} (points : Fin requests → Fin slots → Fin pointCount) : Circuit DeMorgan.signature pointCount requests

Compile one clean flag per request.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.GroupClean.flagsCircuit_size {requests slots pointCount : ℕ} (points : Fin requests → Fin slots → Fin pointCount) : (flagsCircuit points).size = ∑ request : Fin requests, (expression (points request)).gateCount

The exact gate count of flagsCircuit.

theorem Algebraic.MassProduction.Nonuniform.GroupClean.flagsCircuit_eval_iff {requests slots pointCount : ℕ} (points : Fin requests → Fin slots → Fin pointCount) (input : Fin pointCount → Bool) (request : Fin requests) : (flagsCircuit points).eval DeMorgan.interpretation input request = true ↔ ∀ (slot : Fin slots), input (points request slot) = false

No point in a request is conflicting exactly when its clean flag is true.

theorem Algebraic.MassProduction.Nonuniform.GroupClean.flagsCircuit_cost {requests slots pointCount : ℕ} (points : Fin requests → Fin slots → Fin pointCount) : (flagsCircuit points).cost DeMorgan.standardCost = requests * (slots + 1)

Exactly one OR gate per slot and one negation per request.

def Algebraic.MassProduction.Nonuniform.GroupClean.circuit {requests slots pointCount inputs : ℕ} (points : Fin requests → Fin slots → Fin pointCount) (conflicts : Circuit DeMorgan.signature inputs pointCount) : Circuit DeMorgan.signature inputs requests

Aggregate all requests after running the point circuit once.

Equations

• Algebraic.MassProduction.Nonuniform.GroupClean.circuit points conflicts = (Algebraic.MassProduction.Nonuniform.GroupClean.flagsCircuit points).comp conflicts

@[simp]

theorem Algebraic.MassProduction.Nonuniform.GroupClean.circuit_size {requests slots pointCount inputs : ℕ} (points : Fin requests → Fin slots → Fin pointCount) (conflicts : Circuit DeMorgan.signature inputs pointCount) : (circuit points conflicts).size = conflicts.size + (flagsCircuit points).size

The exact gate count of circuit.

theorem Algebraic.MassProduction.Nonuniform.GroupClean.circuit_eval_iff {requests slots pointCount inputs : ℕ} (points : Fin requests → Fin slots → Fin pointCount) (conflicts : Circuit DeMorgan.signature inputs pointCount) (input : Fin inputs → Bool) (request : Fin requests) : (circuit points conflicts).eval DeMorgan.interpretation input request = true ↔ ∀ (slot : Fin slots), conflicts.eval DeMorgan.interpretation input (points request slot) = false

Exact clean-request semantics for a shared point-conflict circuit.

theorem Algebraic.MassProduction.Nonuniform.GroupClean.circuit_cost {requests slots pointCount inputs : ℕ} (points : Fin requests → Fin slots → Fin pointCount) (conflicts : Circuit DeMorgan.signature inputs pointCount) : (circuit points conflicts).cost DeMorgan.standardCost = conflicts.cost DeMorgan.standardCost + requests * (slots + 1)

Only linear work in the number of request-point slots is added.