A conondeterministic lower bound for Boolean inequality

The false inputs of inequality on two n-bit strings are the diagonal assignments (v, v). Above a true input (u, v), the two-point family generated by (u, u) and (v, v) is a semi-ultrafilter and accepts every literal true at (u, v).

As in the row/column inequality graph, a pair cover assigns a Boolean code to every n-bit vertex. Equal codes for distinct vertices would make their canonical semi-ultrafilter preserve the entire cover. Thus every cover has at least n pairs. The universal-circuit pullback transfers this bound, without loss, to conondeterministic AND/OR circuits over literals.

@[reducible, inline]

abbrev Algebraic.Fusion.Conondeterministic.Neq.Vertex (n : ℕ) : Type

An n-bit vertex.

Equations

• Algebraic.Fusion.Conondeterministic.Neq.Vertex n = (Fin n → Bool)

@[reducible, inline]

abbrev Algebraic.Fusion.Conondeterministic.Neq.Assignment (n : ℕ) : Type

A primary assignment consists of two n-bit vertices.

Equations

• Algebraic.Fusion.Conondeterministic.Neq.Assignment n = (Fin (n + n) → Bool)

def Algebraic.Fusion.Conondeterministic.Neq.left {n : ℕ} (assignment : Assignment n) : Vertex n

The left half of a primary assignment.

Equations

• Algebraic.Fusion.Conondeterministic.Neq.left assignment input = assignment (Fin.castAdd n input)

def Algebraic.Fusion.Conondeterministic.Neq.right {n : ℕ} (assignment : Assignment n) : Vertex n

The right half of a primary assignment.

Equations

• Algebraic.Fusion.Conondeterministic.Neq.right assignment input = assignment (Fin.natAdd n input)

def Algebraic.Fusion.Conondeterministic.Neq.pair {n : ℕ} (leftVertex rightVertex : Vertex n) : Assignment n

Pair two vertices into one primary assignment.

Equations

• Algebraic.Fusion.Conondeterministic.Neq.pair leftVertex rightVertex = Algebraic.Fusion.Conondeterministic.combine leftVertex rightVertex

@[simp]

theorem Algebraic.Fusion.Conondeterministic.Neq.left_pair {n : ℕ} (leftVertex rightVertex : Vertex n) : left (pair leftVertex rightVertex) = leftVertex

@[simp]

theorem Algebraic.Fusion.Conondeterministic.Neq.right_pair {n : ℕ} (leftVertex rightVertex : Vertex n) : right (pair leftVertex rightVertex) = rightVertex

def Algebraic.Fusion.Conondeterministic.Neq.function (n : ℕ) (assignment : Assignment n) : Bool

Boolean inequality of the two halves of a primary assignment.

Equations

• Algebraic.Fusion.Conondeterministic.Neq.function n assignment = decide (Algebraic.Fusion.Conondeterministic.Neq.left assignment ≠ Algebraic.Fusion.Conondeterministic.Neq.right assignment)

@[simp]

theorem Algebraic.Fusion.Conondeterministic.Neq.function_pair {n : ℕ} (leftVertex rightVertex : Vertex n) : function n (pair leftVertex rightVertex) = decide (leftVertex ≠ rightVertex)

theorem Algebraic.Fusion.Conondeterministic.Neq.pair_mem_target_iff {n : ℕ} (leftVertex rightVertex : Vertex n) : pair leftVertex rightVertex ∈ (literalProblem (function n)).target ↔ leftVertex ≠ rightVertex

def Algebraic.Fusion.Conondeterministic.Neq.diagonal {n : ℕ} (vertex : Vertex n) : Problem.Outside (literalProblem (function n))

A diagonal false input, regarded as a point outside inequality.

Equations

• Algebraic.Fusion.Conondeterministic.Neq.diagonal vertex = ⟨Algebraic.Fusion.Conondeterministic.Neq.pair vertex vertex, ⋯⟩

@[simp]

theorem Algebraic.Fusion.Conondeterministic.Neq.diagonal_value {n : ℕ} (vertex : Vertex n) : ↑(diagonal vertex) = pair vertex vertex

@[reducible, inline]

abbrev Algebraic.Fusion.Conondeterministic.Neq.canonicalFilter {n : ℕ} (leftVertex rightVertex : Vertex n) : Semifilter (Problem.Outside (literalProblem (function n)))

The canonical two-point semi-filter above an unequal primary input.

Equations

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

theorem Algebraic.Fusion.Conondeterministic.Neq.canonicalFilter_accepts_coordinate {n : ℕ} (leftVertex rightVertex : Vertex n) (coordinate : Fin (n + n)) (value : Bool) (present : pair leftVertex rightVertex coordinate = value) : Problem.restrict (literalProblem (function n)) {assignment : Fin (n + n) → Bool | assignment coordinate = value} ∈ canonicalFilter leftVertex rightVertex

The canonical filter accepts every coordinate condition true at its associated pair.

theorem Algebraic.Fusion.Conondeterministic.Neq.canonicalFilter_above {n : ℕ} (leftVertex rightVertex : Vertex n) : (canonicalFilter leftVertex rightVertex).Above (pair leftVertex rightVertex)

The canonical two-point filter is above its unequal assignment.

theorem Algebraic.Fusion.Conondeterministic.Neq.canonicalFilter_isUltra {n : ℕ} (leftVertex rightVertex : Vertex n) : (canonicalFilter leftVertex rightVertex).IsUltra

Canonical inequality witnesses are semi-ultrafilters.

noncomputable def Algebraic.Fusion.Conondeterministic.Neq.coverCode {n : ℕ} (cover : PairCover (literalProblem (function n)) SemifilterClass.ultra) (vertex : Vertex n) : Fin cover.pairs.length → Bool

Boolean membership code assigned to a diagonal vertex by a pair cover.

Equations

• Algebraic.Fusion.Conondeterministic.Neq.coverCode cover vertex index = Algebraic.AndOr.membership (Algebraic.Fusion.Conondeterministic.Neq.diagonal vertex) (cover.pairs.get index).1

theorem Algebraic.Fusion.Conondeterministic.Neq.coverCode_injective {n : ℕ} (cover : PairCover (literalProblem (function n)) SemifilterClass.ultra) : Function.Injective (coverCode cover)

Every semi-ultrafilter pair cover assigns distinct codes to distinct Boolean vertices.

theorem Algebraic.Fusion.Conondeterministic.Neq.two_pow_le_two_pow_cost {n : ℕ} (cover : PairCover (literalProblem (function n)) SemifilterClass.ultra) : 2 ^ n ≤ 2 ^ cover.cost

Information-theoretic inequality for semi-ultrafilter covers.

theorem Algebraic.Fusion.Conondeterministic.Neq.ultraPairCover_cost_lowerBound {n : ℕ} (cover : PairCover (literalProblem (function n)) SemifilterClass.ultra) : n ≤ cover.cost

Every semi-ultrafilter pair cover for Boolean inequality has at least n pairs.

theorem Algebraic.Fusion.Conondeterministic.Neq.and_lowerBound {n a : ℕ} (circuit : Circuit AndOr.signature (n + n + a + (n + n + a)) 1) (computes : UniversallyComputes circuit (function n)) : n ≤ circuit.cost AndOr.andCost

Any conondeterministic literal circuit universally computing inequality of two n-bit strings contains at least n AND gates, regardless of the number of auxiliary variables or free OR gates.