Documentation

Complexitylib.Algebraic.Basis.DeMorgan.PairIndicator

Two exceptions and input-cube adjacency #

Two exceptions at adjacent inputs form an input subcube and have size at most n. Two exceptions at distance at least two depend on every input and are non-unate, so they require at least n+1 native gates. Both claims also hold for the complemented indicator.

source
def Algebraic.DeMorgan.pairIndicator {n : ℕ} (left right : Fin n → Bool) (value : Bool) :
ScalarFunction Bool n

A Boolean function with the specified value at two inputs and the opposite value elsewhere.

Equations
Instances For
    source
    theorem Algebraic.DeMorgan.pairIndicator_essential {n : ℕ} (left right : Fin n → Bool) (value : Bool) (far : 1 < hammingDist left right) (i : Fin n) :
    EssentialAt (pairIndicator left right value) i

    Every input remains essential when the two exceptions are nonadjacent.

    source
    theorem Algebraic.DeMorgan.pairIndicator_not_unate {n : ℕ} (left right : Fin n → Bool) (value : Bool) (far : 1 < hammingDist left right) :
    ¬Unate (pairIndicator left right value)

    Two nonadjacent exceptions force contradictory influence directions at a differing input.

    source
    theorem Algebraic.DeMorgan.complexity_pairIndicator_ge {n : ℕ} (left right : Fin n → Bool) (value : Bool) (far : 1 < hammingDist left right) :
    n + 1 ≤ complexity (pairIndicator left right value)

    Two nonadjacent exceptions, to either constant, need at least n+1 native gates.

    source
    theorem Algebraic.DeMorgan.complexity_pairIndicator_le_of_adjacent {n : ℕ} (positive : 0 < n) (left right : Fin n → Bool) (value : Bool) (adjacent : BooleanCube.graph.Adj left right) :
    complexity (pairIndicator left right value) ≤ n

    Adjacent exceptions, to either constant, fit within the input-width budget.

    source
    theorem Algebraic.DeMorgan.complexity_pairIndicator_le_iff {n : ℕ} (positive : 0 < n) (left right : Fin n → Bool) (value : Bool) (different : left ≠ right) :
    complexity (pairIndicator left right value) ≤ n ↔ BooleanCube.graph.Adj left right

    At the input-width budget, distinct pairs are cheap exactly when their inputs are adjacent.