Khrapchenko's bound for circuits with shared gates and XOR/EQUIV gates

This file extends the bounds of Complexitylib.Algebraic.LowerBound.KarchmerWigderson.Sharing.Circuit from De Morgan circuits to circuits over Extended.signature, the De Morgan basis together with binary XOR and EQUIV gates.

In SharedProgram.sq_card_edges_le, the Khrapchenko upper bound (k + 1) · X · |A| · |B| depends on X = P.inputLeaves n, which counts only literal leaves on the original circuit inputs 0, …, n - 1 and ignores literal leaves reading shared variables z ≥ n. Consequently, a binary gadget built solely from shared variables z₁, z₂ ≥ n—the four-leaf De Morgan expansion Formula.xorGadget z₁ z₂ of z₁ ⊕ z₂ or Formula.equivGadget z₁ z₂ of z₁ ↔ z₂—has inputLeaves n = 0. Allocating two shared values for the two input wires of each XOR/EQUIV gate and substituting the gadget for the gate wire replaces every XOR/EQUIV gate by a zero-input-leaf subformula while increasing the number of shared values by two, regardless of the gate's fan-out.

Hence a single-output circuit with c_DM AND and OR gates (Extended.deMorganCost), r XOR and EQUIV gates (Extended.xorCost), and k gates of fan-out at least two (sharedGateCount) yields a SharedProgram n K with K ≤ k + 2r and P.inputLeaves n ≤ c_DM + k + 2r + 1 (Extended.exists_sharedProgram_of_circuit). Thus:

• |edges A B|² ≤ (k + 2r + 1) · (c_DM + k + 2r + 1) · |A| · |B| (Extended.sq_card_edges_le_cost),
• n² ≤ (k + 2r + 1) · (c_DM + k + 2r + 1) for parity (Extended.parity_sq_le_cost),
• (n + 1 - t) · t ≤ (k + 2r + 1) · (c_DM + k + 2r + 1) for threshold t (Extended.threshold_mul_le_cost),
• (n - ⌊n/2⌋) · (⌊n/2⌋ + 1) ≤ (k + 2r + 1) · (c_DM + k + 2r + 1) for majority (Extended.majority_mul_le_cost), and both parity and majority require a superlinear number c_DM = ω(n) of AND and OR gates whenever k(n) = o(n) and r(n) = o(n) (Extended.isLittleO_cost_of_parity, Extended.isLittleO_cost_of_majority).

The theorems here carry the names of their De Morgan counterparts in the KW namespace, under KW.Extended; with r = 0 their hypotheses specialize to those of the De Morgan versions. The one difference is majority: Extended.mul_le_cost_of_majority takes 2m + 1 inputs, like KW.mul_le_cost_of_majority, while Extended.mul_le_cost_of_majority_of_four_mul_le and Extended.isLittleO_cost_of_majority cover every input length n, at the price of the factor 4 in the hypothesis 4 · (k + 2r + 1) · (C + 1) ≤ n. (KW.isLittleO_cost_of_majority is stated for the odd lengths 2m + 1 only.)

theorem Algebraic.KW.Extended.exists_sharedProgram_of_circuit {n : ℕ} (c : Circuit signature n 1) {f : Cslib.BooleanFunction n} (hc : c.ComputesWith interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) : ∃ (K : ℕ) (P : SharedProgram n K), K ≤ sharedGateCount c + 2 * c.cost xorCost ∧ P.Computes f ∧ P.inputLeaves n ≤ c.cost deMorganCost + sharedGateCount c + 2 * c.cost xorCost + 1

Extended-basis circuits as programs with shared gates. Every single-output circuit over the extended De Morgan + XOR/EQUIV basis computing f with k gates of fan-out at least two and r XOR/EQUIV gates yields a SharedProgram n K computing f with K ≤ k + 2r and P.inputLeaves n ≤ c_DM + k + 2r + 1, where c_DM counts the AND and OR gates.

Khrapchenko, parity, threshold, and majority lower bounds

theorem Algebraic.KW.Extended.khrapchenkoBound_of_circuit {n k r : ℕ} (c : Circuit signature n 1) {f : Cslib.BooleanFunction n} (hc : c.ComputesWith interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) (hk : sharedGateCount c ≤ k) (hr : c.cost xorCost ≤ r) : KhrapchenkoBound f ((k + 2 * r + 1) * (c.cost deMorganCost + k + 2 * r + 1))

Khrapchenko bound for circuits with k shared gates and r XOR/EQUIV gates. If an extended-basis circuit computes f, at most k of its gates have fan-out at least two, and at most r of its gates are XOR or EQUIV gates, then f satisfies Khrapchenko's bound with measure (k + 2r + 1) · (c_DM + k + 2r + 1), where c_DM counts the AND and OR gates.

theorem Algebraic.KW.Extended.sq_card_edges_le_cost {n k r : ℕ} (c : Circuit signature n 1) {f : Cslib.BooleanFunction n} (hc : c.ComputesWith interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) (hk : sharedGateCount c ≤ k) (hr : c.cost xorCost ≤ r) (A B : Finset (Fin n → Bool)) (hA : ∀ x ∈ A, f x = true) (hB : ∀ y ∈ B, f y = false) : (edges A B).card ^ 2 ≤ (k + 2 * r + 1) * (c.cost deMorganCost + k + 2 * r + 1) * A.card * B.card

Rectangle edge bound for circuits with k shared gates and r XOR/EQUIV gates. If an extended-basis circuit is 1 on A and 0 on B, then |edges A B|² ≤ (k + 2r + 1) · (c_DM + k + 2r + 1) · |A| · |B|.

theorem Algebraic.KW.Extended.parity_sq_le_cost {n : ℕ} [NeZero n] {k r : ℕ} (c : Circuit signature n 1) (computes : c.ComputesWith interpretation (GateElimination.Xor.parityTarget n)) (hk : sharedGateCount c ≤ k) (hr : c.cost xorCost ≤ r) : n ^ 2 ≤ (k + 2 * r + 1) * (c.cost deMorganCost + k + 2 * r + 1)

Parity in circuits with k shared gates and r XOR/EQUIV gates. An extended-basis circuit computing the parity of n ≥ 1 bits satisfies n² ≤ (k + 2r + 1) · (c_DM + k + 2r + 1).

theorem Algebraic.KW.Extended.mul_le_cost_of_parity {n k r C : ℕ} (hkrn : (k + 2 * r + 1) * (C + 1) ≤ n) (c : Circuit signature n 1) (computes : c.ComputesWith interpretation (GateElimination.Xor.parityTarget n)) (hk : sharedGateCount c ≤ k) (hr : c.cost xorCost ≤ r) : C * n ≤ c.cost deMorganCost

Superlinear De Morgan cost for parity with few shared gates and few XOR/EQUIV gates. If (k + 2r + 1) · (C + 1) ≤ n, every extended-basis circuit computing the parity of n bits with at most k gates of fan-out at least two and at most r XOR/EQUIV gates has at least C · n AND and OR gates.

theorem Algebraic.KW.Extended.isLittleO_cost_of_parity {k r : ℕ → ℕ} (hk : (fun (n : ℕ) => ↑(k n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hr : (fun (n : ℕ) => ↑(r n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (c : (n : ℕ) → Circuit signature n 1) (computes : ∀ (n : ℕ), (c n).ComputesWith interpretation (GateElimination.Xor.parityTarget n)) (hshared : ∀ (n : ℕ), sharedGateCount (c n) ≤ k n) (hxor : ∀ (n : ℕ), (c n).cost xorCost ≤ r n) : (fun (n : ℕ) => ↑n) =o[Filter.atTop] fun (n : ℕ) => ↑((c n).cost deMorganCost)

Parity needs superlinear De Morgan gates when k(n) = o(n) and r(n) = o(n). If, for every n, c n is an extended-basis circuit computing the parity of n bits with at most k n = o(n) gates of fan-out at least two and at most r n = o(n) XOR/EQUIV gates, then the number of AND and OR gates of c n grows faster than n.

theorem Algebraic.KW.Extended.threshold_mul_le_cost {n t k r : ℕ} (ht : 1 ≤ t) (htn : t ≤ n) (c : Circuit signature n 1) (computes : c.ComputesWith interpretation (thresholdTarget n t)) (hk : sharedGateCount c ≤ k) (hr : c.cost xorCost ≤ r) : (n + 1 - t) * t ≤ (k + 2 * r + 1) * (c.cost deMorganCost + k + 2 * r + 1)

Threshold functions in circuits with k shared gates and r XOR/EQUIV gates. For 1 ≤ t ≤ n, every extended-basis circuit computing threshold t satisfies (n + 1 - t) · t ≤ (k + 2r + 1) · (c_DM + k + 2r + 1).

theorem Algebraic.KW.Extended.majority_mul_le_cost {n k r : ℕ} (hn : 1 ≤ n) (c : Circuit signature n 1) (computes : c.ComputesWith interpretation (majorityTarget n)) (hk : sharedGateCount c ≤ k) (hr : c.cost xorCost ≤ r) : (n - n / 2) * (n / 2 + 1) ≤ (k + 2 * r + 1) * (c.cost deMorganCost + k + 2 * r + 1)

Majority in circuits with k shared gates and r XOR/EQUIV gates. Every extended-basis circuit computing strict majority of n ≥ 1 bits satisfies (n - ⌊n/2⌋) · (⌊n/2⌋ + 1) ≤ (k + 2r + 1) · (c_DM + k + 2r + 1).

theorem Algebraic.KW.Extended.majority_sq_le_cost_of_odd {n k r : ℕ} (hodd : Odd n) (c : Circuit signature n 1) (computes : c.ComputesWith interpretation (majorityTarget n)) (hk : sharedGateCount c ≤ k) (hr : c.cost xorCost ≤ r) : (n / 2 + 1) ^ 2 ≤ (k + 2 * r + 1) * (c.cost deMorganCost + k + 2 * r + 1)

Odd-input majority in circuits with k shared gates and r XOR/EQUIV gates. For odd n, every extended-basis circuit computing strict majority of n bits satisfies (⌊n/2⌋ + 1)² ≤ (k + 2r + 1) · (c_DM + k + 2r + 1).

theorem Algebraic.KW.Extended.mul_le_cost_of_majority {m k r C : ℕ} (hkrm : (k + 2 * r + 1) * (C + 1) ≤ m) (c : Circuit signature (2 * m + 1) 1) (computes : c.ComputesWith interpretation (majorityTarget (2 * m + 1))) (hk : sharedGateCount c ≤ k) (hr : c.cost xorCost ≤ r) : C * m ≤ c.cost deMorganCost

Superlinear De Morgan cost for odd-input majority with few shared and XOR/EQUIV gates. If (k + 2r + 1) · (C + 1) ≤ m, every extended-basis circuit computing the majority of 2m + 1 bits with at most k gates of fan-out at least two and at most r XOR/EQUIV gates has at least C · m AND and OR gates. With r = 0 this is the hypothesis of KW.mul_le_cost_of_majority; for every input length see mul_le_cost_of_majority_of_four_mul_le.

theorem Algebraic.KW.Extended.mul_le_cost_of_majority_of_four_mul_le {n k r C : ℕ} (hkrn : 4 * (k + 2 * r + 1) * (C + 1) ≤ n) (c : Circuit signature n 1) (computes : c.ComputesWith interpretation (majorityTarget n)) (hk : sharedGateCount c ≤ k) (hr : c.cost xorCost ≤ r) : C * n ≤ c.cost deMorganCost

Superlinear De Morgan cost for majority of any length with few shared and XOR/EQUIV gates. The variant of mul_le_cost_of_majority for every input length n: if 4 · (k + 2r + 1) · (C + 1) ≤ n, every extended-basis circuit computing the majority of n bits with at most k gates of fan-out at least two and at most r XOR/EQUIV gates has at least C · n AND and OR gates.

theorem Algebraic.KW.Extended.isLittleO_cost_of_majority {k r : ℕ → ℕ} (hk : (fun (n : ℕ) => ↑(k n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hr : (fun (n : ℕ) => ↑(r n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (c : (n : ℕ) → Circuit signature n 1) (computes : ∀ (n : ℕ), (c n).ComputesWith interpretation (majorityTarget n)) (hshared : ∀ (n : ℕ), sharedGateCount (c n) ≤ k n) (hxor : ∀ (n : ℕ), (c n).cost xorCost ≤ r n) : (fun (n : ℕ) => ↑n) =o[Filter.atTop] fun (n : ℕ) => ↑((c n).cost deMorganCost)

Majority needs superlinear De Morgan gates when k(n) = o(n) and r(n) = o(n). If, for every input length n, c n is an extended-basis circuit computing the majority of n bits with at most k n = o(n) gates of fan-out at least two and at most r n = o(n) XOR/EQUIV gates, then the number of AND and OR gates of c n grows faster than n. Unlike KW.isLittleO_cost_of_majority, which indexes the family by m with 2m + 1 inputs, the family here ranges over all input lengths.