Signed unbounded AND and XOR circuits

Every operation is either an affine Boolean function or a conjunction of signed inputs with an optional output negation. This includes unbounded AND, OR, XOR, constants, and the full binary basis. Programs use the existing acyclic circuit model: every operation costs one gate and repeated wires and unrestricted fanout are allowed. The geometric count records conjunctions with at least two distinct direct primary inputs, including repeated literals of either polarity.

def Algebraic.Aggregate.Geometry.xorSum {r : ℕ} : (Fin r → Bool) → Bool

Parity of a finite indexed family of bits.

Equations

• Algebraic.Aggregate.Geometry.xorSum x_2 = false
• Algebraic.Aggregate.Geometry.xorSum x_2 = (x_2 0 ^^ Algebraic.Aggregate.Geometry.xorSum (Fin.tail x_2))

inductive Algebraic.Aggregate.Geometry.Op : Type

Affine operations and optionally negated conjunctions of signed literals.

• affine (arity : ℕ) (bias : Bool) (coefficient : Fin arity → Bool) : Op
• conjunction (arity : ℕ) (polarity : Fin arity → Bool) (negated : Bool) : Op

@[reducible, inline]

abbrev Algebraic.Aggregate.Geometry.Op.arity : Op → ℕ

The actual number of input slots of an operation.

Equations

• (Algebraic.Aggregate.Geometry.Op.affine r bias coefficient).arity = r
• (Algebraic.Aggregate.Geometry.Op.conjunction r polarity negated).arity = r

@[reducible, inline]

abbrev Algebraic.Aggregate.Geometry.signature : Signature

Signature for signed AND/OR/XOR circuits.

Equations

• Algebraic.Aggregate.Geometry.signature = { Op := Algebraic.Aggregate.Geometry.Op, Arity := Algebraic.Aggregate.Geometry.Op.arity }

def Algebraic.Aggregate.Geometry.conjunctionValue {r : ℕ} (polarity : Fin r → Bool) (negated : Bool) (x : Fin r → Bool) : Bool

Every conjunction input is a genuine, possibly negated literal.

Equations

• Algebraic.Aggregate.Geometry.conjunctionValue polarity negated x = (negated ^^ decide (∀ (i : Fin r), x i = polarity i))

def Algebraic.Aggregate.Geometry.interpretation : Interpretation signature Bool

Boolean semantics of the signed operations.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Aggregate.Geometry.interpretation (Algebraic.Aggregate.Geometry.Op.conjunction arity polarity negated) x_2 = Algebraic.Aggregate.Geometry.conjunctionValue polarity negated x_2

def Algebraic.Aggregate.Geometry.Op.isConjunction : Op → Bool

Whether the operation uses the conjunction form.

Equations

• (Algebraic.Aggregate.Geometry.Op.affine r bias coefficient).isConjunction = false
• (Algebraic.Aggregate.Geometry.Op.conjunction r polarity negated).isConjunction = true

def Algebraic.Aggregate.Geometry.primaryInputs {n g : ℕ} (line : Line signature n g) : Finset (Fin n)

Distinct original input variables appearing directly among a line's slots.

Equations

• Algebraic.Aggregate.Geometry.primaryInputs line = {i : Fin n | ∃ (slot : Fin (Algebraic.Aggregate.Geometry.signature.Arity line.op)), line.wires slot = Cslib.Circuits.Wire.input i}

def Algebraic.Aggregate.Geometry.multiPrimary {n g : ℕ} (line : Line signature n g) : Bool

Conjunctions with at least two distinct direct original input variables.

Equations

• Algebraic.Aggregate.Geometry.multiPrimary line = (Algebraic.Aggregate.Geometry.Op.isConjunction line.op && decide (2 ≤ (Algebraic.Aggregate.Geometry.primaryInputs line).card))

def Algebraic.Aggregate.Geometry.multiCount {n g : ℕ} : Program signature n g → ℕ

Number of multiple-primary conjunctions in an actual program.

Equations

• Algebraic.Aggregate.Geometry.multiCount Cslib.Circuits.Program.empty = 0
• Algebraic.Aggregate.Geometry.multiCount (p.gate line) = Algebraic.Aggregate.Geometry.multiCount p + if Algebraic.Aggregate.Geometry.multiPrimary line = true then 1 else 0