Enumerating nonuniform affine offsets

All direction/scalar products in a fixed candidate menu can be computed offline. Adding a fixed offset to a binary vector then needs at most one negation per bit. This circuit emits every translated point with a cost linear in the total number of point bits.

def Algebraic.MassProduction.Nonuniform.ConstantTranslations.expression {inputs : ℕ} (offset : Bool) (source : DeMorgan.Wiring inputs) : DeMorgan.Expression inputs

XOR with a hardwired bit uses either a wire or one negation.

Equations

• Algebraic.MassProduction.Nonuniform.ConstantTranslations.expression offset source = if offset = true then source.expression.not else source.expression

theorem Algebraic.MassProduction.Nonuniform.ConstantTranslations.expression_eval {inputs : ℕ} (offset : Bool) (source : DeMorgan.Wiring inputs) (input : Fin inputs → Bool) : DeMorgan.Expression.eval input (expression offset source) = (DeMorgan.Wiring.eval input source ^^ offset)

Exact Boolean translation by a constant offset bit.

theorem Algebraic.MassProduction.Nonuniform.ConstantTranslations.expression_cost_le {inputs : ℕ} (offset : Bool) (source : DeMorgan.Wiring inputs) : (expression offset source).standardCost ≤ 1

At most one charged gate per translated bit.

def Algebraic.MassProduction.Nonuniform.ConstantTranslations.circuit {points width inputs : ℕ} (offsets : Fin points → Fin width → Bool) (sources : Fin points → Fin width → DeMorgan.Wiring inputs) : Circuit DeMorgan.signature inputs (points * width)

Emit all translated points, sharing the source wires freely.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.ConstantTranslations.circuit_size {points width inputs : ℕ} (offsets : Fin points → Fin width → Bool) (sources : Fin points → Fin width → DeMorgan.Wiring inputs) : (circuit offsets sources).size = ∑ point : Fin points, ∑ bit : Fin width, (expression (offsets point bit) (sources point bit)).gateCount

The exact gate count of circuit: the gates of the translated expression of every point and bit.

theorem Algebraic.MassProduction.Nonuniform.ConstantTranslations.circuit_eval {points width inputs : ℕ} (offsets : Fin points → Fin width → Bool) (sources : Fin points → Fin width → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (point : Fin points) (bit : Fin width) : (circuit offsets sources).eval DeMorgan.interpretation input (finProdFinEquiv (point, bit)) = (DeMorgan.Wiring.eval input (sources point bit) ^^ offsets point bit)

Each output point is its source vector XOR its fixed offset.

theorem Algebraic.MassProduction.Nonuniform.ConstantTranslations.circuit_cost_le {points width inputs : ℕ} (offsets : Fin points → Fin width → Bool) (sources : Fin points → Fin width → DeMorgan.Wiring inputs) : (circuit offsets sources).cost DeMorgan.standardCost ≤ points * width

The whole point generator costs at most its number of output bits.