Internals of the negation-limited Boolean matrix product bound

This file reduces De Morgan circuits with few NOT gates computing the Boolean matrix product to the monotone partial-product bound Algebraic.Monotone.MatrixProduct.Internal.card_le_andCost. The surface statements are in Complexitylib.Algebraic.LowerBound.Monotone.MatrixProduct.NegationLimited.

Circuit surgery

• freeze replaces the line of selected gates by constant gates. When every frozen gate already takes its constant value on an assignment, evaluation on that assignment is unchanged (trace_freeze). Freezing only NOT gates keeps the AND-gate count (andCost_freeze) and removes the frozen NOT gates from the NOT-gate count.
• restrictInputs fixes the inputs outside a selected set to a constant by instantiating the circuit after a single constant gate.

Few NOT gates (div_mul_div_mul_le_andCost)

Induction on the bound t on the number of NOT gates. Let G be the first NOT gate. Every wire before it computes a monotone function (isMonotone_trace), in particular its argument h. Let F be the left half of the variables: the rows i < I / 2 of x and the columns j < J / 2 of y, and let c be the value of h on the indicator of F. If c = 0, every assignment that is zero outside F lies below that indicator, so h is zero there; if c = 1, every assignment that is one on F lies above it, so h is one there. Fixing the variables outside F to 0, respectively those of F to 1, therefore makes G constant, so it can be frozen, and keeps a product of (I / 2) × K by K × (J / 2) matrices on the rows and columns whose variables stay free (the first halves if c = 0, the next halves if c = 1). The new circuit has one NOT gate fewer and the same AND gates. With no NOT gate left, the monotone bound gives K * (I / 2 ^ t) * (J / 2 ^ t) AND gates.

NOT gates of few variables (card_le_andCost_of_dependsOnlyOn)

If every NOT gate computes a function of the variables in S, fixing those variables to zero makes every NOT gate constant. Freezing them leaves a circuit without NOT gates computing the partial product over the triples whose variables avoid S, and at most |S| * max I J triples meet S.

Freezing gates to constants

def Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.constLine {n g : ℕ} : Bool → Line DeMorgan.signature n g

The constant gate of value b.

Equations

• Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.constLine false = { op := Algebraic.DeMorgan.Op.false, wires := Fin.elim0 }
• Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.constLine true = { op := Algebraic.DeMorgan.Op.true, wires := Fin.elim0 }

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.constLine_mapWires {n g : ℕ} (b : Bool) {n' g' : ℕ} (f : Wire n g → Wire n' g') : (constLine b).mapWires f = constLine b

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.constLine_eval {n g : ℕ} (b : Bool) (x : Fin n → Bool) (values : Fin g → Bool) : (constLine b).eval DeMorgan.interpretation x values = b

@[simp]

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.andCost_constLine {n g : ℕ} (b : Bool) : DeMorgan.andCost (constLine b).op = 0

@[simp]

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.notCost_constLine {n g : ℕ} (b : Bool) : DeMorgan.notCost (constLine b).op = 0

def Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.freeze {n gates : ℕ} : Program DeMorgan.signature n gates → (Fin gates → Option Bool) → Program DeMorgan.signature n gates

Replace the line of every gate G with sel G = some b by the constant gate b.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.freeze Cslib.Circuits.Program.empty x_3 = Cslib.Circuits.Program.empty

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.lines_freeze {n g : ℕ} (p : Program DeMorgan.signature n g) (sel : Fin g → Option Bool) (G : Fin g) : (freeze p sel).lines G = (sel G).elim (p.lines G) constLine

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.eval_freeze {n g : ℕ} (p : Program DeMorgan.signature n g) (sel : Fin g → Option Bool) (x : Fin n → Bool) (hsel : ∀ (G : Fin g) (b : Bool), sel G = some b → p.eval DeMorgan.interpretation x G = b) : (freeze p sel).eval DeMorgan.interpretation x = p.eval DeMorgan.interpretation x

Freezing gates that already take their constant values does not change the evaluation.

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.trace_freeze {n g : ℕ} (p : Program DeMorgan.signature n g) (sel : Fin g → Option Bool) (x : Fin n → Bool) (hsel : ∀ (G : Fin g) (b : Bool), sel G = some b → p.eval DeMorgan.interpretation x G = b) : (freeze p sel).trace DeMorgan.interpretation x = p.trace DeMorgan.interpretation x

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.cost_freeze {n g : ℕ} (p : Program DeMorgan.signature n g) (sel : Fin g → Option Bool) (cost : OperationCost DeMorgan.signature) : Program.cost cost (freeze p sel) = ∑ G : Fin g, cost ((sel G).elim (p.lines G) constLine).op

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.andCost_freeze {n g : ℕ} (p : Program DeMorgan.signature n g) (sel : Fin g → Option Bool) (hsel : ∀ (G : Fin g) (b : Bool), sel G = some b → (p.lines G).op = DeMorgan.Op.not) : Program.cost DeMorgan.andCost (freeze p sel) = Program.cost DeMorgan.andCost p

Freezing NOT gates keeps the AND-gate count.

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.notCost_freeze_eq_zero {n g : ℕ} (p : Program DeMorgan.signature n g) (sel : Fin g → Option Bool) (hsel : ∀ (G : Fin g), (p.lines G).op = DeMorgan.Op.not → sel G ≠ none) : Program.cost DeMorgan.notCost (freeze p sel) = 0

Freezing every NOT gate leaves none.

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.notCost_freeze_single {n g : ℕ} (p : Program DeMorgan.signature n g) (G₀ : Fin g) (hG₀ : (p.lines G₀).op = DeMorgan.Op.not) (b : Bool) : Program.cost DeMorgan.notCost (freeze p fun (G : Fin g) => if G = G₀ then some b else none) + 1 = Program.cost DeMorgan.notCost p

Freezing one NOT gate removes exactly one NOT gate.

def Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.freezeCircuit {n m : ℕ} (C : Circuit DeMorgan.signature n m) (sel : Fin C.size → Option Bool) : Circuit DeMorgan.signature n m

Freeze the selected gates of a circuit.

Equations

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

Fixing inputs to a constant

def Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.restrictInputs {n m : ℕ} (C : Circuit DeMorgan.signature n m) (keep : Fin n → Bool) (b : Bool) : Circuit DeMorgan.signature n m

Fix every input v with keep v = false to the constant b, read from a single constant gate placed before the circuit.

Equations

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

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.eval_restrictInputs {n m : ℕ} (C : Circuit DeMorgan.signature n m) (keep : Fin n → Bool) (b : Bool) (a : Fin n → Bool) : (restrictInputs C keep b).eval DeMorgan.interpretation a = C.eval DeMorgan.interpretation fun (v : Fin n) => if keep v = true then a v else b

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.cost_restrictInputs {n m : ℕ} (C : Circuit DeMorgan.signature n m) (keep : Fin n → Bool) (b : Bool) (cost : OperationCost DeMorgan.signature) (hcost : cost (constLine b).op = 0) : (restrictInputs C keep b).cost cost = C.cost cost

Wires below the first NOT gate

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.interpretation_of_not {n g : ℕ} (l : Line DeMorgan.signature n g) (hl : l.op = DeMorgan.Op.not) (value : Wire n g → Bool) : (DeMorgan.interpretation l.op fun (a : Fin (DeMorgan.arity l.op)) => value (l.wires a)) = !value (l.wires ⟨0, ⋯⟩)

A NOT gate computes the negation of its argument.

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.isMonotone_trace {n g : ℕ} (p : Program DeMorgan.signature n g) (B : ℕ) (hB : ∀ (G : Fin g), ↑G < B → (p.lines G).op ≠ DeMorgan.Op.not) (w : Wire n g) (hw : ↑w.index < n + B) : Internal.IsMonotone fun (a : Fin n → Bool) => p.trace DeMorgan.interpretation a w

Every wire before the first NOT gate computes a monotone function.

Halving

def Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.leftHalf {N I J K : ℕ} (L : Internal.Layout N I J K) (v : Fin N) : Bool

The left half of the variables: rows i < I / 2 of x and columns j < J / 2 of y.

Equations

• Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.leftHalf L v = decide ((∃ (i : Fin I) (k : Fin K), ↑i < I / 2 ∧ L.x i k = v) ∨ ∃ (k : Fin K) (j : Fin J), ↑j < J / 2 ∧ L.y k j = v)

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.leftHalf_x {N I J K : ℕ} (L : Internal.Layout N I J K) (i : Fin I) (k : Fin K) : leftHalf L (L.x i k) = decide (↑i < I / 2)

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.leftHalf_y {N I J K : ℕ} (L : Internal.Layout N I J K) (k : Fin K) (j : Fin J) : leftHalf L (L.y k j) = decide (↑j < J / 2)

def Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.half {I : ℕ} (b : Bool) (i : Fin (I / 2)) : Fin I

The kept half of Fin I: the first I / 2 indices when b = false, the next I / 2 when b = true.

Equations

• Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.half b i = ⟨(bif b then I / 2 else 0) + ↑i, ⋯⟩

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.half_lt_iff {I : ℕ} (b : Bool) (i : Fin (I / 2)) : ↑(half b i) < I / 2 ↔ b = false

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.half_injective {I : ℕ} (b : Bool) : Function.Injective (half b)

def Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.halveLayout {N I J K : ℕ} (L : Internal.Layout N I J K) (b : Bool) : Internal.Layout N (I / 2) (J / 2) K

The layout of the kept rows and columns.

Equations

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

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.exists_halve {N M I J K : ℕ} (L : Internal.Layout N I J K) (z : Fin I → Fin J → Fin M) (C : Circuit DeMorgan.signature N M) (computes : ∀ (a : Fin N → Bool) (i : Fin I) (j : Fin J), C.eval DeMorgan.interpretation a (z i j) = decide (∃ (k : Fin K), a (L.x i k) = true ∧ a (L.y k j) = true)) (hnot : 0 < C.cost DeMorgan.notCost) : ∃ (L' : Internal.Layout N (I / 2) (J / 2) K) (z' : Fin (I / 2) → Fin (J / 2) → Fin M) (C' : Circuit DeMorgan.signature N M), C'.cost DeMorgan.notCost + 1 = C.cost DeMorgan.notCost ∧ C'.cost DeMorgan.andCost = C.cost DeMorgan.andCost ∧ ∀ (a : Fin N → Bool) (i : Fin (I / 2)) (j : Fin (J / 2)), C'.eval DeMorgan.interpretation a (z' i j) = decide (∃ (k : Fin K), a (L'.x i k) = true ∧ a (L'.y k j) = true)

One NOT gate can be traded for halving the numbers of rows and columns.

Few NOT gates

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.div_mul_div_mul_le_andCost {N K : ℕ} (t : ℕ) {I J : ℕ} (L : Internal.Layout N I J K) {M : ℕ} (z : Fin I → Fin J → Fin M) (C : Circuit DeMorgan.signature N M) : C.cost DeMorgan.notCost ≤ t → (∀ (a : Fin N → Bool) (i : Fin I) (j : Fin J), C.eval DeMorgan.interpretation a (z i j) = decide (∃ (k : Fin K), a (L.x i k) = true ∧ a (L.y k j) = true)) → I / 2 ^ t * (J / 2 ^ t) * K ≤ C.cost DeMorgan.andCost

Few NOT gates. A De Morgan circuit with at most t NOT gates computing the product of an I × K matrix and a K × J matrix, laid out injectively among its inputs, has at least (I / 2 ^ t) * (J / 2 ^ t) * K AND gates.

NOT gates of few variables

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.mul_mul_le_card_add {N I J K : ℕ} (L : Internal.Layout N I J K) (S : Finset (Fin N)) : I * J * K ≤ {t : Fin I × Fin K × Fin J | L.x t.1 t.2.1 ∉ S ∧ L.y t.2.1 t.2.2 ∉ S}.card + S.card * max I J

At most |S| * max I J triples have a variable in S.

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.mul_mul_le_andCost_add {N M I J K : ℕ} (L : Internal.Layout N I J K) (z : Fin I → Fin J → Fin M) (C : Circuit DeMorgan.signature N M) (computes : ∀ (a : Fin N → Bool) (i : Fin I) (j : Fin J), C.eval DeMorgan.interpretation a (z i j) = decide (∃ (k : Fin K), a (L.x i k) = true ∧ a (L.y k j) = true)) (S : Finset (Fin N)) (local_ : ∀ (G : Fin C.size), (C.program.lines G).op = DeMorgan.Op.not → DependsOnlyOn (C.program.gateFunction DeMorgan.interpretation G) S) : I * J * K ≤ C.cost DeMorgan.andCost + S.card * max I J

NOT gates of few variables. If every NOT gate of a De Morgan circuit computing the product of an I × K matrix and a K × J matrix computes a function of the variables in S, the circuit has at least I * J * K - |S| * max I J AND gates.

Non-monotone gates of few variables

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.eq_bot_of_monotone_of_antitone {N : ℕ} {f : (Fin N → Bool) → Bool} (hm : Monotone f) (ha : Antitone f) (a : Fin N → Bool) : f a = f ⊥

A function on assignments that is both monotone and antitone is constant.

theorem Algebraic.Monotone.MatrixProduct.NegationLimited.Internal.dependsOnlyOn_of_not {N M : ℕ} (C : Circuit DeMorgan.signature N M) (S : Finset (Fin N)) (localized : ∀ (G : Fin C.size), Monotone (C.program.gateFunction DeMorgan.interpretation G) ∨ DependsOnlyOn (C.program.gateFunction DeMorgan.interpretation G) S) (G : Fin C.size) (hG : (C.program.lines G).op = DeMorgan.Op.not) : DependsOnlyOn (C.program.gateFunction DeMorgan.interpretation G) S

If every gate computing a non-monotone function depends only on the inputs in S, so does every NOT gate.