An AND-gate lower bound for crown-graph collision

The crown graph on two copies of Fin N joins a left vertex to a right vertex exactly when their labels differ. Its graph-collision function asks whether some marked left vertex and some marked right vertex are adjacent.

On assignments marking exactly one vertex on each side, graph collision is Boolean inequality. Pulling the positive-generator set problem back to this one-hot slice therefore gives Neq.problem N exactly, and the inequality lower bound transfers to monotone AND/OR circuits computing graph collision.

def Algebraic.Fusion.CrownCollision.function {N : ℕ} (assignment : Fin (N + N) → Bool) : Bool

The graph-collision function for the crown graph K_{N,N} with the diagonal perfect matching removed.

Equations

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

@[reducible, inline]

abbrev Algebraic.Fusion.CrownCollision.problem (N : ℕ) : SetProblem (Fin (N + N) → Bool)

The positive-generator set problem for crown-graph collision.

Equations

• Algebraic.Fusion.CrownCollision.problem N = Algebraic.Fusion.monotoneProblem Algebraic.Fusion.CrownCollision.function

def Algebraic.Fusion.CrownCollision.oneHotPair {N : ℕ} (edge : Neq.Ground N) : Fin (N + N) → Bool

Mark exactly the two vertices selected by an ordered left/right pair.

Equations

• Algebraic.Fusion.CrownCollision.oneHotPair edge i = Fin.addCases (fun (left : Fin N) => decide (left = edge.1)) (fun (right : Fin N) => decide (right = edge.2)) i

theorem Algebraic.Fusion.CrownCollision.preimage_eq_neq {N : ℕ} : Problem.map (problem N) (AndOr.preimageHomomorphism oneHotPair).map = Neq.problem N

Pulling crown-graph collision back to one-hot left/right assignments gives the row/column inequality problem exactly.

theorem Algebraic.Fusion.CrownCollision.and_lowerBound {n : ℕ} (circuit : Circuit AndOr.signature (2 ^ n + 2 ^ n) 1) (computes : ∀ (assignment : Fin (2 ^ n + 2 ^ n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function assignment) : n ≤ circuit.cost AndOr.andCost

Every AND/OR circuit computing crown-graph collision on two copies of Fin (2 ^ n) uses at least n AND gates, even when OR gates are free.