Independent nonlinear output components

Boolean functions are viewed as vectors over the two-element field. Affine primary functions form a submodule; independence modulo this submodule records that no nonzero linear combination of output coordinates is affine in the original inputs.

def Algebraic.Aggregate.Geometry.bitValue (b : Bool) : ZMod 2

A Boolean value in the two-element field.

Equations

• Algebraic.Aggregate.Geometry.bitValue b = if b = true then 1 else 0

def Algebraic.Aggregate.Geometry.bitVector {n : ℕ} (x : Fin n → Bool) : Fin n → ZMod 2

The original input bits in prime-field coordinates.

Equations

• Algebraic.Aggregate.Geometry.bitVector x i = Algebraic.Aggregate.Geometry.bitValue (x i)

def Algebraic.Aggregate.Geometry.affineFunctions (n : ℕ) : Submodule (ZMod 2) ((Fin n → Bool) → ZMod 2)

The submodule of affine functions of the original input coordinates.

Equations

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

def Algebraic.Aggregate.Geometry.NonaffineComponents {n m : ℕ} (F : (Fin n → Bool) → Fin m → Bool) : Prop

Every nonzero linear combination of output bits is nonaffine in the primary bits.

Equations

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

def Algebraic.Aggregate.Geometry.conjunctionCount {n g : ℕ} (p : Program signature n g) : ℕ

Number of conjunction operations, including signed and constant conjunctions.

Equations

• Algebraic.Aggregate.Geometry.conjunctionCount p = {gate : Fin g | Algebraic.Aggregate.Geometry.Op.isConjunction (p.lines gate).op = true}.card