The deterministic lifting theorem

A protocol of depth c for a search problem R lifted by the index gadget gives a decision tree for R of depth d with (m / τ) ^ d ≤ 4 ^ c, whenever 4 ≤ τ, τ ^ 2 ≤ m and 320 n ^ 2 (⌊log₂ m⌋ + 1) ≤ τ (Communication.Lifting.exists_decisionTree_of_solves). With τ = √m this reads d log₂ m ≤ 4 c (Communication.Lifting.depth_mul_logb_le). Together with the simulation of decision trees by protocols (Communication.Lifting.ecomplexity_lift_le), the communication complexity of the lifted problem is Θ(log m) times the decision-tree depth of R once √m ≥ 320 n ^ 2 (⌊log₂ m⌋ + 1), which holds for some m = O(n ^ 4 log² n) Raz and McKenzie, Göös, Pitassi and Watson, Theorem 3.

The decision tree walks down the protocol (Communication.Lifting.sim), keeping a rectangle X × Y of inputs that reach the current node, a set J of queried coordinates and their answers ρ (Communication.Lifting.SimState) Mertz and Pitassi, Algorithm 2. The invariants (Communication.Lifting.SimState.Good) are:

• every pair in X × Y gives the gadget the values ρ on J, and both sets are fixed on J;
• X is τ-dense on the other coordinates, and Y has small deficiency on their blocks;
• X is large, which bounds the number of queries.

When Bob speaks, the tree follows the larger half of Y. When Alice speaks, it follows the larger half of X and splits it by the density-restoring partition. It chooses a piece (I, α, P) leaving every value on I possible for many y (Communication.Lifting.exists_piece_forall_le_card_filter), queries the coordinates I, and fixes Bob's blocks of I accordingly (Communication.Lifting.exists_fix_blocks). At a leaf, the full-range lemma (Communication.Lifting.exists_forall_eq_of_isDense) shows that the protocol's output answers R on every input consistent with the queries. A query of #I coordinates shrinks X by a factor of about τ ^ #I, while a uniform set would shrink by m ^ #I. Since X loses at most a factor 4 per bit sent, (m / τ) ^ d ≤ 4 ^ c.

Mertz and Pitassi need only m ≥ n ^ (1 + ε), using the blockwise approximate sunflower lemma in the full-range lemma. The elementary Janson-type bound used here needs m of order n ^ 4. Both are polynomial in n, as in the statement of Göös, Pitassi and Watson.

Main definitions

• Cslib.Communication.Lifting.SimState: the state of the simulation.
• Cslib.Communication.Lifting.sim: the simulating decision tree.

Main results

• Cslib.Communication.Lifting.exists_decisionTree_of_solves: the lifting theorem.
• Cslib.Communication.Lifting.depth_mul_logb_le: the lifting theorem with τ = √m.

References

• I. Mertz and T. Pitassi, Lifting: As Easy As 1, 2, 3
• M. Göös, T. Pitassi and T. Watson, Deterministic communication vs. partition number
• R. Raz and P. McKenzie, Separation of the monotone NC hierarchy

def Cslib.Communication.Lifting.bigHalf {α : Type u_2} (s : Finset α) (f : α → Bool) : Bool

The larger half of s under the bit f: at least half of s has f a = bigHalf s f.

theorem Cslib.Communication.Lifting.card_le_two_mul_card_filter_bigHalf {α : Type u_2} (s : Finset α) (f : α → Bool) : ↑s.card ≤ 2 * ↑{a ∈ s | f a = bigHalf s f}.card

theorem Cslib.Communication.Lifting.card_le_pow_of_fixed {n m : ℕ} {J : Finset (Fin n)} {X : Finset (Fin n → Fin m)} (hX : ∀ x ∈ X, ∀ x' ∈ X, ∀ i ∈ J, x i = x' i) : X.card ≤ m ^ Jᶜ.card

A set fixed on J has at most m ^ #Jᶜ pointer vectors.

structure Cslib.Communication.Lifting.SimState (n m : ℕ) : Type

The state of the simulation: the queried coordinates J with answers ρ, the rectangle X × Y, and the number t of bits simulated so far.

• J : Finset (Fin n)

  The queried coordinates.

• ρ : Fin n → Bool

  The answers to the queries, on J.

• X : Finset (Fin n → Fin m)

  Alice's inputs.

• Y : Finset (Fin n → Fin m → Bool)

  Bob's inputs.

• t : ℕ

  The number of bits simulated.

structure Cslib.Communication.Lifting.SimState.Good {n m : ℕ} {O : Type u_1} (τ : ℝ) (c : ℕ) (R : (Fin n → Bool) → O → Prop) (p : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O) (st : SimState n m) : Prop

The invariants of the simulation of the protocol p, with density τ and total budget c Mertz and Pitassi, invariants (i)–(iii).

• X_nonempty : st.X.Nonempty
• X_fixed (x : Fin n → Fin m) : x ∈ st.X → ∀ x' ∈ st.X, ∀ i ∈ st.J, x i = x' i
• Y_fixed (y : Fin n → Fin m → Bool) : y ∈ st.Y → ∀ y' ∈ st.Y, ∀ i ∈ st.J, y i = y' i
• ind_eq (x : Fin n → Fin m) : x ∈ st.X → ∀ y ∈ st.Y, ∀ i ∈ st.J, y i (x i) = st.ρ i
• dense : IsDense τ st.Jᶜ st.X
• Y_large : 2 ^ (st.Jᶜ.card * m) ≤ 2 ^ st.t * (4 * τ) ^ st.J.card * ↑st.Y.card
• X_large : ↑m ^ st.Jᶜ.card * (↑m / τ) ^ st.J.card ≤ 4 ^ st.t * ↑st.X.card
• solves : p.Solves (lift R) ↑st.X ↑st.Y
• budget : st.t + p.depth ≤ c

theorem Cslib.Communication.Lifting.SimState.Good.pow_le {n m : ℕ} {O : Type u_1} {τ : ℝ} {c : ℕ} {R : (Fin n → Bool) → O → Prop} {p : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O} {st : SimState n m} (h : Good τ c R p st) : (↑m / τ) ^ st.J.card ≤ 4 ^ st.t

The queries made so far are paid for: (m / τ) ^ #J ≤ 4 ^ t.

theorem Cslib.Communication.Lifting.SimState.Good.two_pow_le {n m : ℕ} {O : Type u_1} {τ : ℝ} {c : ℕ} {R : (Fin n → Bool) → O → Prop} {p : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O} {st : SimState n m} (h : Good τ c R p st) (hτ4 : 4 ≤ τ) (hτm : τ ^ 2 ≤ ↑m) : 2 ^ (st.Jᶜ.card * m) ≤ 2 ^ (5 * st.t) * ↑st.Y.card

The deficiency of Y is at most 5 t bits.

theorem Cslib.Communication.Lifting.SimState.Good.output {n m : ℕ} {O : Type u_1} {τ : ℝ} {c : ℕ} {R : (Fin n → Bool) → O → Prop} {st : SimState n m} {o : O} (h : Good τ c R (Protocol.output o) st) (hτ4 : 4 ≤ τ) (hτm : τ ^ 2 ≤ ↑m) (hτc : 64 * ↑n * (5 * ↑c + 2) ≤ τ) (z : Fin n → Bool) (hz : ∀ i ∈ st.J, z i = st.ρ i) : R z o

At a leaf, the protocol's output answers R on every input consistent with the queries, by the full-range lemma.

theorem Cslib.Communication.Lifting.SimState.Good.bob {n m : ℕ} {O : Type u_1} {τ : ℝ} {c : ℕ} {R : (Fin n → Bool) → O → Prop} {st : SimState n m} {send : (Fin n → Fin m → Bool) → Bool} {p₀ p₁ : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O} (h : Good τ c R (Protocol.bob send p₀ p₁) st) (hτ : 0 < τ) (b : Bool) (hb : ↑st.Y.card ≤ 2 * ↑{y ∈ st.Y | send y = b}.card) : Good τ c R (bif b then p₁ else p₀) { J := st.J, ρ := st.ρ, X := st.X, Y := {y ∈ st.Y | send y = b}, t := st.t + 1 }

When Bob speaks, following a half of Y holding at least half of it keeps the invariants.

theorem Cslib.Communication.Lifting.SimState.Good.alice {n m : ℕ} {O : Type u_1} {τ : ℝ} {c : ℕ} {R : (Fin n → Bool) → O → Prop} {st : SimState n m} {send : (Fin n → Fin m) → Bool} {p₀ p₁ : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O} (h : Good τ c R (Protocol.alice send p₀ p₁) st) (hτ : 0 < τ) (b : Bool) (hb : ↑st.X.card ≤ 2 * ↑{x ∈ st.X | send x = b}.card) {L : List (Piece n m)} (hL : IsPartition τ st.Jᶜ ({x ∈ st.X | send x = b}) L) {q : Piece n m} (hqL : q ∈ L) (hq : ∀ (β : Fin n → Bool), ↑st.Y.card ≤ ↑(allowing st.Y q.I q.α β).card * (4 * τ) ^ q.I.card) (ρ' : Fin n → Bool) (hρ' : ∀ i ∈ st.J, ρ' i = st.ρ i) (η : Fin n → Fin m → Bool) (hη : ∀ i ∈ q.I, η i (q.α i) = ρ' i) (hηcard : ↑(allowing st.Y q.I q.α ρ').card ≤ ↑{y ∈ st.Y | ∀ i ∈ q.I, y i = η i}.card * 2 ^ (m * q.I.card)) : Good τ c R (bif b then p₁ else p₀) { J := st.J ∪ q.I, ρ := ρ', X := q.P, Y := {y ∈ st.Y | ∀ i ∈ q.I, y i = η i}, t := st.t + 1 }

When Alice speaks, following a half of X holding at least half of it, restricting to a good piece (I, α, P) of its density-restoring partition, and fixing Bob's blocks of I to blocks η giving the answers ρ' keeps the invariants.

The simulating decision tree

noncomputable def Cslib.Communication.Lifting.partitionOf {n m : ℕ} (τ : ℝ) (F : Finset (Fin n)) (X : Finset (Fin n → Fin m)) : List (Piece n m)

The density-restoring partition used by the simulation.

theorem Cslib.Communication.Lifting.isPartition_partitionOf {n m : ℕ} {τ : ℝ} (hτ : 0 < τ) (F : Finset (Fin n)) (X : Finset (Fin n → Fin m)) : IsPartition τ F X (partitionOf τ F X)

def Cslib.Communication.Lifting.GoodPiece {n m : ℕ} (τ : ℝ) (Y : Finset (Fin n → Fin m → Bool)) (q : Piece n m) : Prop

A piece leaving every value β on its fixed coordinates possible for a (4 τ) ^ (-#I) fraction of Y.

def Cslib.Communication.Lifting.mergeAnswers {n : ℕ} (I : Finset (Fin n)) (ρ' ρ : Fin n → Bool) : Fin n → Bool

The answers ρ' on I and ρ elsewhere.

noncomputable def Cslib.Communication.Lifting.fixBlocks {n m : ℕ} (Y : Finset (Fin n → Fin m → Bool)) (I : Finset (Fin n)) (α : Fin n → Fin m) (β : Fin n → Bool) : Fin n → Fin m → Bool

Bob's blocks fixed in Phase II.

def Cslib.Communication.Lifting.SimState.afterBob {n m : ℕ} (st : SimState n m) (send : (Fin n → Fin m → Bool) → Bool) : SimState n m

The state after Bob speaks: the larger half of Y.

noncomputable def Cslib.Communication.Lifting.SimState.afterAlice {n m : ℕ} (st : SimState n m) (q : Piece n m) (ρ' : Fin n → Bool) : SimState n m

The state after Alice speaks and the coordinates of the piece q are queried with answers ρ'.

noncomputable def Cslib.Communication.Lifting.sim {n m : ℕ} {O : Type u_1} (τ : ℝ) : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O → SimState n m → DecisionTree (Fin n) O

The simulating decision tree Mertz and Pitassi, Algorithm 2.

theorem Cslib.Communication.Lifting.SimState.Good.afterAlice {n m : ℕ} {O : Type u_1} {τ : ℝ} {c : ℕ} {R : (Fin n → Bool) → O → Prop} {st : SimState n m} {send : (Fin n → Fin m) → Bool} {p₀ p₁ : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O} (h : Good τ c R (Protocol.alice send p₀ p₁) st) (hτ : 0 < τ) {q : Piece n m} (hq : q ∈ partitionOf τ st.Jᶜ ({x ∈ st.X | send x = bigHalf st.X send})) (hgood : GoodPiece τ st.Y q) (ρ' : Fin n → Bool) : Good τ c R (bif bigHalf st.X send then p₁ else p₀) (st.afterAlice q ρ')

The Alice step: the state after the query keeps the invariants.

theorem Cslib.Communication.Lifting.SimState.Good.exists_goodPiece {n m : ℕ} {O : Type u_1} {τ : ℝ} {c : ℕ} {R : (Fin n → Bool) → O → Prop} {st : SimState n m} {send : (Fin n → Fin m) → Bool} {p₀ p₁ : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O} (h : Good τ c R (Protocol.alice send p₀ p₁) st) (hτ4 : 4 ≤ τ) (hτm : τ ^ 2 ≤ ↑m) (hτc : 64 * ↑n * (5 * ↑c + 2) ≤ τ) : ∃ q ∈ partitionOf τ st.Jᶜ ({x ∈ st.X | send x = bigHalf st.X send}), GoodPiece τ st.Y q

Under the invariants, some piece of the partition is good.

theorem Cslib.Communication.Lifting.eval_sim {n m : ℕ} {O : Type u_1} {τ : ℝ} {c : ℕ} {R : (Fin n → Bool) → O → Prop} (hτ4 : 4 ≤ τ) (hτm : τ ^ 2 ≤ ↑m) (hτc : 64 * ↑n * (5 * ↑c + 2) ≤ τ) (p : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O) (st : SimState n m) : SimState.Good τ c R p st → ∀ (z : Fin n → Bool), (∀ i ∈ st.J, z i = st.ρ i) → R z ((sim τ p st).eval z)

Correctness of the simulation.

theorem Cslib.Communication.Lifting.pow_depth_sim {n m : ℕ} {O : Type u_1} {τ : ℝ} {c : ℕ} {R : (Fin n → Bool) → O → Prop} (hτ4 : 4 ≤ τ) (hτm : τ ^ 2 ≤ ↑m) (hτc : 64 * ↑n * (5 * ↑c + 2) ≤ τ) (p : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O) (st : SimState n m) : SimState.Good τ c R p st → (↑m / τ) ^ (st.J.card + (sim τ p st).depth) ≤ 4 ^ (st.t + p.depth)

The number of queries of the simulation: (m / τ) ^ (#J + depth) ≤ 4 ^ (t + depth p).

The lifting theorem

def Cslib.Communication.Lifting.SimState.init (n m : ℕ) : SimState n m

The initial state: nothing queried, all inputs.

theorem Cslib.Communication.Lifting.isDense_univ {n m : ℕ} {τ : ℝ} (hτ : 0 ≤ τ) (hτm : τ ≤ ↑m) (F : Finset (Fin n)) : IsDense τ F Finset.univ

All of [m]ⁿ is τ-dense when τ ≤ m.

theorem Cslib.Communication.Lifting.exists_decisionTree_of_solves {n m : ℕ} {O : Type u_1} {R : (Fin n → Bool) → O → Prop} {τ : ℝ} (hτ4 : 4 ≤ τ) (hτm : τ ^ 2 ≤ ↑m) (hτn : 320 * ↑n ^ 2 * (↑(Nat.log 2 m) + 1) ≤ τ) {p : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O} (hp : p.Solves (lift R) Set.univ Set.univ) : ∃ (t : DecisionTree (Fin n) O), (∀ (z : Fin n → Bool), R z (t.eval z)) ∧ (↑m / τ) ^ t.depth ≤ 4 ^ p.depth

The deterministic lifting theorem Raz and McKenzie, Göös, Pitassi and Watson, Theorem 3, Mertz and Pitassi, Lemma 3.1. Let 4 ≤ τ, τ ^ 2 ≤ m and 320 n ^ 2 (⌊log₂ m⌋ + 1) ≤ τ. If a protocol of depth c solves the lifted search problem lift R on all inputs, then a decision tree of depth d with (m / τ) ^ d ≤ 4 ^ c solves R.

theorem Cslib.Communication.Lifting.depth_mul_logb_le {n m : ℕ} {O : Type u_1} {R : (Fin n → Bool) → O → Prop} (hm : 16 ≤ m) (hmn : 320 * ↑n ^ 2 * (↑(Nat.log 2 m) + 1) ≤ √↑m) {p : Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O} (hp : p.Solves (lift R) Set.univ Set.univ) : ∃ (t : DecisionTree (Fin n) O), (∀ (z : Fin n → Bool), R z (t.eval z)) ∧ ↑t.depth * Real.logb 2 ↑m ≤ 4 * ↑p.depth

The deterministic lifting theorem with τ = √m. If m ≥ 16 and 320 n ^ 2 (⌊log₂ m⌋ + 1) ≤ √m, then every protocol of depth c solving the lifted search problem gives a decision tree of depth d with d log₂ m ≤ 4 c.