Sharp native gate bounds for input subcube indicators

Positive literals are collected in one conjunction and negative literals in one negated disjunction. A nonempty mask on k input coordinates, or its complement, therefore needs at most k native gates.

def Algebraic.DeMorgan.allInputs {n : ℕ} (coordinates : Finset (Fin n)) : ScalarFunction Bool n

Conjunction of selected positive input literals.

Equations

• Algebraic.DeMorgan.allInputs coordinates input = decide (∀ i ∈ coordinates, input i = true)

def Algebraic.DeMorgan.anyInput {n : ℕ} (coordinates : Finset (Fin n)) : ScalarFunction Bool n

Disjunction of selected positive input literals.

Equations

• Algebraic.DeMorgan.anyInput coordinates input = decide (∃ i ∈ coordinates, input i = true)

theorem Algebraic.DeMorgan.complexity_allInputs_add_one_le {n : ℕ} (coordinates : Finset (Fin n)) (nonempty : coordinates.Nonempty) : complexity (allInputs coordinates) + 1 ≤ coordinates.card

A nonempty conjunction of k inputs needs at most k-1 gates.

theorem Algebraic.DeMorgan.complexity_anyInput_add_one_le {n : ℕ} (coordinates : Finset (Fin n)) (nonempty : coordinates.Nonempty) : complexity (anyInput coordinates) + 1 ≤ coordinates.card

A nonempty disjunction of k inputs needs at most k-1 gates.

def Algebraic.DeMorgan.mask {n : ℕ} (coordinates : Finset (Fin n)) (pattern : Fin n → Bool) (value : Bool) : ScalarFunction Bool n

Output value exactly on inputs matching the specified coordinates.

Equations

• Algebraic.DeMorgan.mask coordinates pattern value input = if ∀ i ∈ coordinates, input i = pattern i then value else !value

theorem Algebraic.DeMorgan.complexity_mask_le {n : ℕ} (coordinates : Finset (Fin n)) (pattern : Fin n → Bool) (value : Bool) : complexity (mask coordinates pattern value) ≤ max 1 coordinates.card

A mask or its complement costs at most one gate per fixed input, except for the empty mask.

theorem Algebraic.DeMorgan.complexity_point_indicator_le {n : ℕ} (positive : 0 < n) (point : Fin n → Bool) (value : Bool) : (complexity fun (input : Fin n → Bool) => if input = point then value else !value) ≤ n

Every single exception to either constant has a circuit of size at most the input width.