From 90ce2e25eeb263fd67aac9f299cfddf01ebafc24 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 01:01:48 +0000 Subject: [PATCH 01/23] feat(communication): nondeterministic communication complexity by covers Nondeterministic.ecomplexity z R A B for relations (least k with a z-cover by 2^k rectangles) and ecomplexityFun at the graph of a function, relation-first as agreed in #1599; fooling-set and rectangle-size bounds, negation, monotonicity, and N^z <= D. Second PR of #1599. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../Communication/Nondeterministic/Basic.lean | 323 ++++++++++++++++++ .../NondeterministicCommunication.lean | 126 +++++++ 3 files changed, 450 insertions(+) create mode 100644 Complexity/Computability/Communication/Nondeterministic/Basic.lean create mode 100644 ComplexityTests/NondeterministicCommunication.lean diff --git a/Complexity.lean b/Complexity.lean index f08f52b9d..ff3f15e45 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -979,6 +979,7 @@ public import Complexity.Computability.Communication.Lifting.Gadget public import Complexity.Computability.Communication.Lifting.Partition public import Complexity.Computability.Communication.Lifting.Simulation public import Complexity.Computability.Communication.Newman +public import Complexity.Computability.Communication.Nondeterministic.Basic public import Complexity.Computability.Communication.Operations public import Complexity.Computability.Communication.Protocol public import Complexity.Computability.Communication.Randomized diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean new file mode 100644 index 000000000..dc4555bf4 --- /dev/null +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -0,0 +1,323 @@ +/- +Copyright (c) 2026 András Z. Salamon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: András Z. Salamon +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Communication.FoolingSet +public import Complexity.Computability.Communication.Rectangle +public import Complexity.Foundations.Data.BitString.Basic + +/-! +# Nondeterministic communication complexity + +Nondeterministic communication complexity for the answer `z : Bool` is defined by covers +[Kushilevitz and Nisan, Chapter 2][KushilevitzNisan1997]. For a relation `R : X → Y → Bool → Prop`, +a *`z`-cover* of `R` on `A × B` by `2 ^ k` rectangles is a family of rectangles indexed by the +`k`-bit guesses such that `z` is an acceptable answer on the part of each rectangle inside `A × B`, +and every pair of `A × B` on which `!z` is not acceptable lies in some rectangle +(`Nondeterministic.IsCover`). The complexity `Nondeterministic.ecomplexity z R A B` is the least +such `k`, or `⊤` if there is none; in particular it is `⊤` if no answer is acceptable on some pair +of `A × B`, as for `Protocol.ecomplexity`. For a function `f : X → Y → Bool`, +`Nondeterministic.ecomplexityFun z f A B` is the complexity of the relation `f x y = b`; its +`z`-covers are families of rectangles on which `f` is `z` inside `A × B` that contain every pair of +`A × B` on which `f` is `z` +(`Nondeterministic.isCover_fun_iff`). Thus `ecomplexityFun true f` and `ecomplexityFun false f` are +`⌈log₂ C^z(f)⌉`, where `C^z(f)` is the least number of rectangles in a `z`-cover (and `0` when `f` +never takes the value `z` on `A × B`): `N¹` and `N⁰` in the cover (certificate) definition, rounded +up to an integer. + +A partial function is a function together with the sets `A` and `B`: its value outside `A × B` does +not matter, and rectangles are not required to lie inside `A × B`. A partial function whose domain +is not a rectangle is a relation that accepts every answer outside its domain. + +## Covers and protocols + +A nondeterministic protocol of cost `c` gives a cover by at most `2 ^ c` rectangles, so lower bounds +on `ecomplexity` hold for every protocol convention. Protocol definitions differ from this one by +at most an additive constant, so an upper bound here is slightly weaker than an upper bound for +protocols. Conversely, a cover by `2 ^ k` rectangles gives a protocol: guess `k` bits naming a +rectangle, Alice sends one bit saying whether her input is in its first side, and Bob accepts when +both inputs are in it, for cost `k + 1`, or `k + 2` if Bob's answer is counted as a sent bit. So a +nondeterministic protocol of cost `c` proves `ecomplexity z R A B ≤ c` once it is converted to a +cover by `2 ^ c` rectangles (`Nondeterministic.ecomplexity_le_iff`). Deterministic protocols give +such covers directly: `Nondeterministic.ecomplexity_le_protocol`. + +## Main definitions + +* `Cslib.Communication.Nondeterministic.IsCover`, `Cslib.Communication.Nondeterministic.HasCover`: + covers of a relation by rectangles. +* `Cslib.Communication.Nondeterministic.ecomplexity`: nondeterministic communication complexity of a + relation on `A × B` for the answer `z`. +* `Cslib.Communication.Nondeterministic.ecomplexityFun`: the same for a function, as the relation + `f x y = b`. + +## Main results + +* `Cslib.Communication.Nondeterministic.ecomplexity_le_iff`, + `Cslib.Communication.Nondeterministic.le_ecomplexity_iff`, + `Cslib.Communication.Nondeterministic.HasCover.ecomplexity_le`: upper and lower bounds through + covers; `Cslib.Communication.Nondeterministic.ecomplexityFun_le_iff` and + `Cslib.Communication.Nondeterministic.le_ecomplexityFun_iff` for functions. +* `Cslib.Communication.Nondeterministic.isCover_fun_iff`: covers of a function. +* `Cslib.Communication.Nondeterministic.HasCover.mono_bits`: more guessed bits do no harm. +* `Cslib.Communication.Nondeterministic.HasCover.mono`, + `Cslib.Communication.Nondeterministic.ecomplexity_mono`, + `Cslib.Communication.Nondeterministic.ecomplexityFun_mono`: monotonicity in the domain. +* `Cslib.Communication.Nondeterministic.HasCover.of_imp`, + `Cslib.Communication.Nondeterministic.ecomplexity_le_of_imp`: a weaker relation is no harder. +* `Cslib.Communication.Nondeterministic.ecomplexity_not`, + `Cslib.Communication.Nondeterministic.ecomplexityFun_not`: `N⁰` is `N¹` of the negation. +* `Cslib.Communication.Nondeterministic.HasCover.card_le`, + `Cslib.Communication.Nondeterministic.le_ecomplexityFun_of_isFoolingSet`: a fooling set of + `2 ^ n` pairs with value `z` forces `n`. +* `Cslib.Communication.Nondeterministic.HasCover.card_le_two_pow_mul`: if every `z`-rectangle has + at most `K` pairs, then a `z`-cover by `2 ^ k` rectangles covers at most `2 ^ k * K` pairs. +* `Cslib.Communication.Nondeterministic.hasCover_of_solves`, + `Cslib.Communication.Nondeterministic.ecomplexity_le_protocol`, + `Cslib.Communication.Nondeterministic.ecomplexityFun_le_protocol`: nondeterministic complexity is + at most deterministic complexity. + +## References + +* [E. Kushilevitz, N. Nisan, *Communication Complexity*][KushilevitzNisan1997] +-/ + +@[expose] public section + +namespace Cslib.Communication + +namespace Nondeterministic + +open Finset + +variable {X Y : Type*} + +/-- `C` is a `z`-cover of the relation `R` on `A × B` by `2 ^ k` rectangles: `z` is an acceptable +answer on the part of each rectangle inside `A × B`, and every pair of `A × B` on which `!z` is not +acceptable lies in some rectangle. -/ +def IsCover (R : X → Y → Bool → Prop) (z : Bool) (A : Set X) (B : Set Y) {k : ℕ} + (C : BitString k → Set X × Set Y) : Prop := + (∀ w, ∀ x ∈ A, x ∈ (C w).1 → ∀ y ∈ B, y ∈ (C w).2 → R x y z) ∧ + ∀ x ∈ A, ∀ y ∈ B, ¬R x y (!z) → ∃ w, x ∈ (C w).1 ∧ y ∈ (C w).2 + +/-- The relation `R` has a `z`-cover on `A × B` by `2 ^ k` rectangles. -/ +def HasCover (R : X → Y → Bool → Prop) (z : Bool) (A : Set X) (B : Set Y) (k : ℕ) : Prop := + ∃ C : BitString k → Set X × Set Y, IsCover R z A B C + +/-- The nondeterministic communication complexity of the relation `R` on `A × B` for the answer +`z`: the least `k` such that `R` has a `z`-cover on `A × B` by `2 ^ k` rectangles, or `⊤` if there +is none. -/ +noncomputable def ecomplexity (z : Bool) (R : X → Y → Bool → Prop) (A : Set X) (B : Set Y) : ℕ∞ := + ⨅ k : {k : ℕ // HasCover R z A B k}, (k.1 : ℕ∞) + +/-- The nondeterministic communication complexity of `f` on `A × B` for the value `z`: +`ecomplexity` of the relation `f x y = b`. `N¹` is `z = true`, and `N⁰` is `z = false`. -/ +noncomputable def ecomplexityFun (z : Bool) (f : X → Y → Bool) (A : Set X) (B : Set Y) : ℕ∞ := + ecomplexity z (fun x y b => f x y = b) A B + +variable {R R' : X → Y → Bool → Prop} {f : X → Y → Bool} {z : Bool} {A A' : Set X} {B B' : Set Y} + {j k : ℕ} + +/-- A `z`-cover of a function: `f` is `z` on the part of each rectangle inside `A × B`, and every +pair of `A × B` on which `f` is `z` lies in some rectangle. -/ +theorem isCover_fun_iff {C : BitString k → Set X × Set Y} : + IsCover (fun x y b => f x y = b) z A B C ↔ + (∀ w, ∀ x ∈ A, x ∈ (C w).1 → ∀ y ∈ B, y ∈ (C w).2 → f x y = z) ∧ + ∀ x ∈ A, ∀ y ∈ B, f x y = z → ∃ w, x ∈ (C w).1 ∧ y ∈ (C w).2 := by + simp only [IsCover, Bool.eq_not, not_not] + +/-! ### Upper and lower bounds -/ + +/-- A cover by `2 ^ k` rectangles bounds the complexity by `k`. -/ +theorem HasCover.ecomplexity_le (h : HasCover R z A B k) : ecomplexity z R A B ≤ k := + iInf_le (fun k : {k : ℕ // HasCover R z A B k} => (k.1 : ℕ∞)) ⟨k, h⟩ + +/-- A cover by `2 ^ j` rectangles gives one by `2 ^ k` rectangles for `j ≤ k`: ignore the extra +guessed bits. -/ +theorem HasCover.mono_bits (hjk : j ≤ k) (h : HasCover R z A B j) : HasCover R z A B k := by + obtain ⟨C, hmem, hcov⟩ := h + refine ⟨fun w => C fun i => w (Fin.castLE hjk i), fun w => hmem _, fun x hx y hy hR => ?_⟩ + obtain ⟨w, hw⟩ := hcov x hx y hy hR + refine ⟨fun i => if hi : (i : ℕ) < j then w ⟨i, hi⟩ else false, ?_⟩ + simpa using hw + +/-- Lower bounds on nondeterministic complexity are lower bounds on the number of guessed bits of +every cover. -/ +theorem le_ecomplexity_iff {c : ℕ∞} : + c ≤ ecomplexity z R A B ↔ ∀ k, HasCover R z A B k → c ≤ k := by + simp [ecomplexity, le_iInf_iff, Subtype.forall] + +/-- `R` has nondeterministic complexity at most `k` exactly when it has a `z`-cover by `2 ^ k` +rectangles. -/ +theorem ecomplexity_le_iff : ecomplexity z R A B ≤ k ↔ HasCover R z A B k := by + refine ⟨fun h => ?_, HasCover.ecomplexity_le⟩ + have : Nonempty {k : ℕ // HasCover R z A B k} := by + rw [← ENat.iInf_natCast_ne_top] + exact ne_top_of_le_ne_top (ENat.natCast_ne_top k) h + obtain ⟨⟨j, hj⟩, hmin⟩ := ENat.exists_eq_iInf + (fun k : {k : ℕ // HasCover R z A B k} => (k.1 : ℕ∞)) + exact hj.mono_bits (by exact_mod_cast (hmin.trans_le h : (j : ℕ∞) ≤ k)) + +/-- `ecomplexity_le_iff` for functions. -/ +theorem ecomplexityFun_le_iff : + ecomplexityFun z f A B ≤ k ↔ HasCover (fun x y b => f x y = b) z A B k := + ecomplexity_le_iff + +/-- `le_ecomplexity_iff` for functions. -/ +theorem le_ecomplexityFun_iff {c : ℕ∞} : + c ≤ ecomplexityFun z f A B ↔ ∀ k, HasCover (fun x y b => f x y = b) z A B k → c ≤ k := + le_ecomplexity_iff + +/-! ### Monotonicity -/ + +/-- A cover on `A × B` is a cover on any smaller domain. -/ +theorem HasCover.mono (hA : A' ⊆ A) (hB : B' ⊆ B) (h : HasCover R z A B k) : + HasCover R z A' B' k := by + obtain ⟨C, hmem, hcov⟩ := h + exact ⟨C, fun w x hx hxC y hy hyC => hmem w x (hA hx) hxC y (hB hy) hyC, + fun x hx y hy hR => hcov x (hA hx) y (hB hy) hR⟩ + +/-- A cover of `R` is a cover of every weaker relation. -/ +theorem HasCover.of_imp (hR : ∀ x y b, R x y b → R' x y b) (h : HasCover R z A B k) : + HasCover R' z A B k := by + obtain ⟨C, hmem, hcov⟩ := h + exact ⟨C, fun w x hx hxC y hy hyC => hR x y z (hmem w x hx hxC y hy hyC), + fun x hx y hy hR' => hcov x hx y hy fun h => hR' (hR x y _ h)⟩ + +/-- Nondeterministic complexity is monotone in the domain. -/ +theorem ecomplexity_mono (hA : A' ⊆ A) (hB : B' ⊆ B) : + ecomplexity z R A' B' ≤ ecomplexity z R A B := + le_ecomplexity_iff.mpr fun _ hk => (hk.mono hA hB).ecomplexity_le + +/-- `ecomplexity_mono` for functions. -/ +theorem ecomplexityFun_mono (hA : A' ⊆ A) (hB : B' ⊆ B) : + ecomplexityFun z f A' B' ≤ ecomplexityFun z f A B := + ecomplexity_mono hA hB + +/-- A weaker relation is no harder. -/ +theorem ecomplexity_le_of_imp (hR : ∀ x y b, R x y b → R' x y b) : + ecomplexity z R' A B ≤ ecomplexity z R A B := + le_ecomplexity_iff.mpr fun _ hk => (hk.of_imp hR).ecomplexity_le + +/-! ### Negation -/ + +/-- Exchanging the answers exchanges `N⁰` and `N¹`. -/ +theorem ecomplexity_not : + ecomplexity z (fun x y b => R x y (!b)) A B = ecomplexity (!z) R A B := by + have hiff : ∀ k, HasCover (fun x y b => R x y (!b)) z A B k ↔ HasCover R (!z) A B k := fun k => by + simp only [HasCover, IsCover, Bool.not_not] + exact le_antisymm (le_ecomplexity_iff.mpr fun k hk => ((hiff k).mpr hk).ecomplexity_le) + (le_ecomplexity_iff.mpr fun k hk => ((hiff k).mp hk).ecomplexity_le) + +/-- `N⁰` of `f` is `N¹` of its negation, and conversely. -/ +@[simp] theorem ecomplexityFun_not : + ecomplexityFun z (fun x y => !f x y) A B = ecomplexityFun (!z) f A B := by + rw [ecomplexityFun, ecomplexityFun, ← ecomplexity_not] + simp only [Bool.not_eq_eq_eq_not] + +/-! ### Lower bounds -/ + +/-- **The fooling-set bound, for covers.** A fooling set for `f` with value `z` inside `A × B` +has at most `2 ^ k` pairs if `f` has a `z`-cover on `A × B` by `2 ^ k` rectangles: no rectangle +contains two of its pairs. -/ +theorem HasCover.card_le {S : Finset (X × Y)} (hS : IsFoolingSet f z S) + (hSAB : ∀ q ∈ S, q.1 ∈ A ∧ q.2 ∈ B) (h : HasCover (fun x y b => f x y = b) z A B k) : + #S ≤ 2 ^ k := by + classical + obtain ⟨C, hC⟩ := h + obtain ⟨hmem, hcov⟩ := isCover_fun_iff.mp hC + have hw : ∀ q ∈ S, ∃ w, q.1 ∈ (C w).1 ∧ q.2 ∈ (C w).2 := fun q hq => + hcov _ (hSAB q hq).1 _ (hSAB q hq).2 (hS.1 q hq) + choose! g hg using hw + calc #S ≤ #(univ : Finset (BitString k)) := by + refine card_le_card_of_injOn g (by intro _ _; exact mem_univ _) ?_ + intro q hq q' hq' hqq + refine hS.2 q hq q' hq' ?_ ?_ + · exact hmem (g q) _ (hSAB q hq).1 (hg q hq).1 _ (hSAB q' hq').2 + (by rw [hqq]; exact (hg q' hq').2) + · exact hmem (g q) _ (hSAB q' hq').1 (by rw [hqq]; exact (hg q' hq').1) _ + (hSAB q hq).2 (hg q hq).2 + _ = 2 ^ k := by rw [card_univ, BitString.card] + +/-- **The fooling-set bound on nondeterministic complexity.** A fooling set of at least `2 ^ n` +pairs for `f` with value `z` inside `A × B` forces `n`. -/ +theorem le_ecomplexityFun_of_isFoolingSet {S : Finset (X × Y)} (hS : IsFoolingSet f z S) + (hSAB : ∀ q ∈ S, q.1 ∈ A ∧ q.2 ∈ B) {n : ℕ} (hn : 2 ^ n ≤ #S) : + (n : ℕ∞) ≤ ecomplexityFun z f A B := + le_ecomplexityFun_iff.mpr fun _ hk => by + have := hn.trans (hk.card_le hS hSAB) + exact_mod_cast (Nat.pow_le_pow_iff_right (by norm_num)).mp this + +/-- **The rectangle-size bound.** If `f` is `z` on at most `K` pairs of every rectangle on which it +is constantly `z`, then a `z`-cover by `2 ^ k` rectangles covers at most `2 ^ k * K` pairs. -/ +theorem HasCover.card_le_two_pow_mul [Fintype X] [Fintype Y] {K : ℕ} + (hK : ∀ (S : Finset X) (T : Finset Y), (∀ x ∈ S, ∀ y ∈ T, f x y = z) → #S * #T ≤ K) + (h : HasCover (fun x y b => f x y = b) z Set.univ Set.univ k) : + #{q : X × Y | f q.1 q.2 = z} ≤ 2 ^ k * K := by + classical + obtain ⟨C, hC⟩ := h + obtain ⟨hmem, hcov⟩ := isCover_fun_iff.mp hC + let S : BitString k → Finset X := fun w => {x | x ∈ (C w).1} + let T : BitString k → Finset Y := fun w => {y | y ∈ (C w).2} + have hsub : ({q : X × Y | f q.1 q.2 = z} : Finset (X × Y)) ⊆ + univ.biUnion fun w => S w ×ˢ T w := by + intro q hq + simp only [mem_filter, mem_univ, true_and] at hq + obtain ⟨w, hx, hy⟩ := hcov q.1 trivial q.2 trivial hq + simp only [mem_biUnion, mem_univ, true_and, mem_product] + exact ⟨w, by simpa [S] using hx, by simpa [T] using hy⟩ + calc #{q : X × Y | f q.1 q.2 = z} ≤ #(univ.biUnion fun w => S w ×ˢ T w) := card_le_card hsub + _ ≤ ∑ w, #(S w ×ˢ T w) := card_biUnion_le + _ ≤ ∑ _w : BitString k, K := by + refine sum_le_sum fun w _ => ?_ + rw [card_product] + refine hK _ _ fun x hx y hy => hmem w x trivial ?_ y trivial ?_ + · simpa [S] using hx + · simpa [T] using hy + _ = 2 ^ k * K := by rw [sum_const, card_univ, BitString.card, smul_eq_mul] + +/-! ### Comparison with deterministic complexity -/ + +/-- The leaves with output `z` of a deterministic protocol solving `R` on `A × B` form a `z`-cover +of `R` by `2 ^ depth` rectangles. -/ +theorem hasCover_of_solves {p : Protocol X Y Bool} (hp : p.Solves R A B) (z : Bool) : + HasCover R z A B p.depth := by + classical + let e := BitString.equivFin p.depth + refine ⟨fun w => if h : (e w : ℕ) < p.leafCount then + if p.leafOutput ⟨e w, h⟩ = z then (p.leafAlice ⟨e w, h⟩, p.leafBob ⟨e w, h⟩) else (∅, ∅) + else (∅, ∅), fun w x hxA hx y hyB hy => ?_, fun x hxA y hyB hR => ?_⟩ + · by_cases h : (e w : ℕ) < p.leafCount + · by_cases hz : p.leafOutput ⟨e w, h⟩ = z + · simp only [h, hz, dite_true, ite_true] at hx hy + have := hp x hxA y hyB + rwa [Protocol.run_eq_leafOutput hx hy, hz] at this + · simp [h, hz] at hx + · simp [h] at hx + · have hlt : (p.leaf x y : ℕ) < 2 ^ p.depth := + (p.leaf x y).2.trans_le p.leafCount_le_two_pow_depth + refine ⟨e.symm ⟨p.leaf x y, hlt⟩, ?_⟩ + have hrun : p.run x y = z := by + have := hp x hxA y hyB + cases hb : p.run x y <;> cases z <;> simp_all + have hz : p.leafOutput (p.leaf x y) = z := by rw [← Protocol.run_eq_leafOutput_leaf, hrun] + simp only [Equiv.apply_symm_apply, (p.leaf x y).2, dite_true, Fin.eta, hz, ite_true] + exact ⟨Protocol.mem_leafAlice_leaf, Protocol.mem_leafBob_leaf⟩ + +/-- **Nondeterministic complexity is at most deterministic complexity.** -/ +theorem ecomplexity_le_protocol (z : Bool) : + ecomplexity z R A B ≤ Protocol.ecomplexity R A B := + le_iInf fun p => (hasCover_of_solves p.2 z).ecomplexity_le + +/-- `ecomplexity_le_protocol` for functions on all inputs. -/ +theorem ecomplexityFun_le_protocol (z : Bool) : + ecomplexityFun z f Set.univ Set.univ ≤ Protocol.ecomplexityFun f := + ecomplexity_le_protocol z + +end Nondeterministic + +end Cslib.Communication diff --git a/ComplexityTests/NondeterministicCommunication.lean b/ComplexityTests/NondeterministicCommunication.lean new file mode 100644 index 000000000..42d98fe9f --- /dev/null +++ b/ComplexityTests/NondeterministicCommunication.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2026 András Z. Salamon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: András Z. Salamon +-/ + +import Complexity.Computability.Communication.Functions +import Complexity.Computability.Communication.Nondeterministic.Basic + +/-! Tests for nondeterministic communication complexity by covers: exact values for equality on +three values (`N¹ = 2 = ⌈log₂ 3⌉`, by an explicit cover and the rectangle-size bound) and on `Bool` +(`N⁰ = 1`, by an explicit cover and a fooling set, and `N¹` of inequality by negation); smaller +domains that make equality trivial; a relation with several acceptable answers, which is easier +than the function it relaxes, and one with none, which has no cover; and bounds by deterministic +protocols, for a function and for a relation. -/ + +namespace ComplexityTests.NondeterministicCommunication + +open Finset Cslib Cslib.Communication Cslib.Communication.Nondeterministic + +/-! ### Equality on three values -/ + +/-- The rectangles of equality on `Fin 3` on which it is `true` have at most one pair. -/ +private theorem card_mul_le_one_of_equality (S T : Finset (Fin 3)) + (h : ∀ x ∈ S, ∀ y ∈ T, equality x y = true) : #S * #T ≤ 1 := by + revert h + decide +revert + +-- `N¹(EQ)` on `Fin 3` is `2`: three diagonal pairs need more than `2 ^ 1` rectangles, and the +-- diagonal singletons indexed by two bits are a cover. +example : ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) Set.univ Set.univ = 2 := by + refine le_antisymm (ecomplexityFun_le_iff.mpr ?_) (le_ecomplexityFun_iff.mpr fun k hk => ?_) + · let e := BitString.equivFin 2 + refine ⟨fun w => ({x | (x : ℕ) = e w}, {y | (y : ℕ) = e w}), isCover_fun_iff.mpr ⟨?_, ?_⟩⟩ + · intro w x _ hx y _ hy + simp only [Set.mem_ofPred_eq] at hx hy + simp [equality, Fin.ext_iff, hx, hy] + · intro x _ y _ h + simp only [equality, decide_eq_true_eq] at h + exact ⟨e.symm ⟨x, by omega⟩, by simp, by simp [h]⟩ + · have := hk.card_le_two_pow_mul card_mul_le_one_of_equality + have h3 : #{q : Fin 3 × Fin 3 | equality q.1 q.2 = true} = 3 := by decide + rw [h3, mul_one] at this + have : 2 ≤ k := by + by_contra! hk + interval_cases k <;> simp at this + exact_mod_cast this + +/-- On the smaller domain `{0} × Fin 3` one rectangle suffices. -/ +private theorem ecomplexityFun_equality_zero_univ : + ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) {0} Set.univ = 0 := + nonpos_iff_eq_zero.mp <| ecomplexityFun_le_iff.mpr ⟨fun _ => ({0}, {0}), isCover_fun_iff.mpr + ⟨fun _ x hx _ y _ hy => by simp_all [equality], + fun x hx y _ h => ⟨0, hx, by simp_all [equality]⟩⟩⟩ + +-- So it does on any smaller domain. +example : ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) {0} {0, 1} = 0 := + nonpos_iff_eq_zero.mp <| (ecomplexityFun_mono le_rfl (Set.subset_univ _)).trans + ecomplexityFun_equality_zero_univ.le + +/-! ### Equality on `Bool` -/ + +/-- `N⁰(EQ)` on `Bool` is `1`: `(false, true)` and `(true, false)` form a fooling set with value +`false`, and `{b} × {!b}` for the two bits `b` are a cover. -/ +private theorem ecomplexityFun_false_equality_bool : + ecomplexityFun false (equality : Bool → Bool → Bool) Set.univ Set.univ = 1 := by + refine le_antisymm (ecomplexityFun_le_iff.mpr ?_) ?_ + · refine ⟨fun w => ({w 0}, {!w 0}), isCover_fun_iff.mpr ⟨?_, ?_⟩⟩ + · intro w x _ hx y _ hy + simp only [Set.mem_singleton_iff] at hx hy + simp [equality, hx, hy] + · intro x _ y _ h + refine ⟨fun _ => x, rfl, ?_⟩ + cases x <;> cases y <;> simp_all [equality] + · refine le_ecomplexityFun_of_isFoolingSet (S := {(false, true), (true, false)}) ?_ (by simp) + (by decide) + simp [IsFoolingSet, equality] + +example : ecomplexityFun false (equality : Bool → Bool → Bool) Set.univ Set.univ = 1 := + ecomplexityFun_false_equality_bool + +-- Negation exchanges the answers: `N¹` of inequality is `N⁰` of equality. +example : ecomplexityFun true (fun x y : Bool => !equality x y) Set.univ Set.univ = 1 := by + rw [ecomplexityFun_not, Bool.not_true, ecomplexityFun_false_equality_bool] + +/-! ### Relations -/ + +/-- Equality under the promise `x = y`: off the diagonal every answer is acceptable. -/ +private def promiseEq (x y : Bool) (b : Bool) : Prop := x = y → b = true + +-- No pair must be covered with `false`, since `true` is acceptable everywhere: one empty +-- rectangle is a `0`-cover, although `N⁰` of equality itself is `1`. +example : ecomplexity false promiseEq Set.univ Set.univ = 0 := + nonpos_iff_eq_zero.mp <| ecomplexity_le_iff.mpr + ⟨fun _ => (∅, ∅), fun _ _ _ hx => hx.elim, fun _ _ _ _ h => (h fun _ => rfl).elim⟩ + +-- The relation is weaker than equality, so it is no harder. +example : ecomplexity false promiseEq Set.univ Set.univ ≤ + ecomplexityFun false (equality : Bool → Bool → Bool) Set.univ Set.univ := + ecomplexity_le_of_imp fun _ _ b h hxy => by simp_all [equality] + +-- A relation with no acceptable answer has no cover, as it has no protocol. +example : ecomplexity true (fun (_ _ _ : Bool) => False) Set.univ Set.univ = ⊤ := + top_le_iff.mp <| le_ecomplexity_iff.mpr fun _ ⟨C, hmem, hcov⟩ => by + obtain ⟨w, hx, hy⟩ := hcov false trivial false trivial id + exact (hmem w _ trivial hx _ trivial hy).elim + +/-! ### Deterministic protocols -/ + +/-- Alice sends her bit, then Bob sends whether his bit is equal. -/ +private def eqProtocol : Protocol Bool Bool Bool := + .alice id (.bob id (.output true) (.output false)) (.bob id (.output false) (.output true)) + +-- The protocol computes equality with two bits, so `N¹(EQ) ≤ 2` on `Bool`. +example : ecomplexityFun true (equality : Bool → Bool → Bool) Set.univ Set.univ ≤ 2 := + (ecomplexityFun_le_protocol true).trans <| + (Protocol.ecomplexityFun_le_depth (p := eqProtocol) + (funext₂ fun x y => by cases x <;> cases y <;> rfl)).trans (by decide) + +-- The relation `promiseEq` is solved without communication, so its `N¹` is `0`. +example : ecomplexity true promiseEq Set.univ Set.univ = 0 := + nonpos_iff_eq_zero.mp <| (ecomplexity_le_protocol true).trans <| + (Protocol.ecomplexity_le_depth (p := .output true) (R := promiseEq) (A := Set.univ) + (B := Set.univ) fun _ _ _ _ _ => rfl).trans (by simp) + +end ComplexityTests.NondeterministicCommunication From a2059b25ee99dd4fff258e66a1fa416b408fd171 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 01:01:48 +0000 Subject: [PATCH 02/23] feat(communication): nondeterministic complexity of equality, disjointness and inner product N^1(EQ_v) = N^1(DISJ_v) = N^0(NDISJ_v) = v; N^1(IP_v) >= v - 1 and N^0(IP_v) >= v via Lindsey's lemma. Third PR of #1599; stacked on nondeterministic-communication. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../Nondeterministic/Functions.lean | 157 ++++++++++++++++++ .../NondeterministicFunctions.lean | 46 +++++ 3 files changed, 204 insertions(+) create mode 100644 Complexity/Computability/Communication/Nondeterministic/Functions.lean create mode 100644 ComplexityTests/NondeterministicFunctions.lean diff --git a/Complexity.lean b/Complexity.lean index ff3f15e45..407574475 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -980,6 +980,7 @@ public import Complexity.Computability.Communication.Lifting.Partition public import Complexity.Computability.Communication.Lifting.Simulation public import Complexity.Computability.Communication.Newman public import Complexity.Computability.Communication.Nondeterministic.Basic +public import Complexity.Computability.Communication.Nondeterministic.Functions public import Complexity.Computability.Communication.Operations public import Complexity.Computability.Communication.Protocol public import Complexity.Computability.Communication.Randomized diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean new file mode 100644 index 000000000..cbbd62b55 --- /dev/null +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -0,0 +1,157 @@ +/- +Copyright (c) 2026 András Z. Salamon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: András Z. Salamon +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Communication.Functions +public import Complexity.Foundations.BooleanAnalysis.HadamardRectangles +public import Complexity.Foundations.Data.Code.Hadamard +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +public import Complexity.Computability.Communication.Nondeterministic.Basic + +/-! +# Nondeterministic complexity of equality, disjointness and inner product + +Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bit strings +[Kushilevitz and Nisan, Chapters 1–3][KushilevitzNisan1997]: + +* equality: `N¹(EQ_v) = v`, from the fooling set of diagonal pairs and the cover by diagonal + singletons [Kushilevitz and Nisan, Examples 1.21 and 2.5][KushilevitzNisan1997]; +* disjointness: `N¹(DISJ_v) = v`, from the fooling set of complementary pairs and the cover by the + rectangles `{x ⊆ w} × {y ⊆ wᶜ}`, so `N⁰(NDISJ_v) = v` for its negation; +* inner product modulo two: `N¹(IP_v) ≥ v - 1` and `N⁰(IP_v) ≥ v`. By Lindsey's + lemma a rectangle on which the inner product is constant has at most `2^v` pairs + (`BitString.card_mul_le_two_pow_of_dotProduct_eq`), while the inner product is `1` on + `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. + +## Main results + +* `Cslib.Communication.Nondeterministic.ecomplexityFun_equality` +* `Cslib.Communication.Nondeterministic.ecomplexityFun_disjointness` +* `Cslib.Communication.Nondeterministic.ecomplexityFun_not_disjointness` +* `Cslib.Communication.Nondeterministic.HasCover.card_dotProduct_le` +* `Cslib.Communication.Nondeterministic.le_ecomplexityFun_true_dotProduct` +* `Cslib.Communication.Nondeterministic.le_ecomplexityFun_false_dotProduct` + +## References + +* [E. Kushilevitz, N. Nisan, *Communication Complexity*][KushilevitzNisan1997] +-/ + +@[expose] public section + +namespace Cslib.Communication + +namespace Nondeterministic + +open Finset + +variable {v : ℕ} + +/-! ### Equality and disjointness -/ + +/-- `N¹(EQ_v) = v`: the `2 ^ v` diagonal pairs form a fooling set, and the `2 ^ v` diagonal +singletons `{w} × {w}` form a `1`-cover. -/ +theorem ecomplexityFun_equality (v : ℕ) : + ecomplexityFun true (equality : BitString v → BitString v → Bool) Set.univ Set.univ = v := by + refine le_antisymm (ecomplexityFun_le_iff.mpr + ⟨fun w => ({w}, {w}), isCover_fun_iff.mpr ⟨fun w x _ hx y _ hy => ?_, fun x _ y _ h => ?_⟩⟩) ?_ + · simp only [Set.mem_singleton_iff] at hx hy + simp [equality, hx, hy] + · simp only [equality, decide_eq_true_eq] at h + exact ⟨x, rfl, h.symm⟩ + · exact le_ecomplexityFun_of_isFoolingSet (isFoolingSet_equality univ) (by simp) + (by rw [card_image_of_injective _ fun x y h => congrArg Prod.fst h, card_univ, + BitString.card]) + +/-- `N¹(DISJ_v) = v`: the `2 ^ v` complementary pairs form a fooling set, and the rectangles +`{x ⊆ w} × {y ⊆ wᶜ}` for the `2 ^ v` sets `w` form a `1`-cover. -/ +theorem ecomplexityFun_disjointness (v : ℕ) : + ecomplexityFun true (disjointness : BitString v → BitString v → Bool) Set.univ Set.univ = + v := by + refine le_antisymm (ecomplexityFun_le_iff.mpr + ⟨fun w => ({x | ∀ i, x i = true → w i = true}, {y | ∀ i, y i = true → w i = false}), + isCover_fun_iff.mpr ⟨fun w x _ hx y _ hy => ?_, fun x _ y _ h => ?_⟩⟩) ?_ + · simp only [Set.mem_ofPred_eq] at hx hy + simp only [disjointness, decide_eq_true_eq, Bool.and_eq_false_iff] + intro i + cases hxi : x i + · simp + · cases hyi : y i + · simp + · simpa [hx i hxi] using hy i hyi + · simp only [disjointness, decide_eq_true_eq, Bool.and_eq_false_iff] at h + refine ⟨x, fun i hi => hi, fun i hi => ?_⟩ + simpa [hi] using h i + · exact le_ecomplexityFun_of_isFoolingSet (isFoolingSet_disjointness univ) (by simp) + (by rw [card_image_of_injective _ fun x y h => congrArg Prod.fst h, card_univ, + BitString.card]) + +/-- `N⁰(NDISJ_v) = N¹(DISJ_v) = v`. -/ +theorem ecomplexityFun_not_disjointness (v : ℕ) : + ecomplexityFun false (fun a b : BitString v => !disjointness a b) Set.univ Set.univ = v := by + rw [ecomplexityFun_not, Bool.not_false, ecomplexityFun_disjointness] + +/-! ### Inner product -/ + +/-- A `z`-cover of the inner product by `2 ^ k` rectangles covers at most `2 ^ k * 2 ^ v` pairs. -/ +theorem HasCover.card_dotProduct_le {k : ℕ} {z : Bool} + (hk : HasCover (fun (x y : BitString v) b => x ⬝ᵥ y = b) z Set.univ Set.univ k) : + #{q : BitString v × BitString v | q.1 ⬝ᵥ q.2 = z} ≤ 2 ^ k * 2 ^ v := + hk.card_le_two_pow_mul fun S T h => by + simpa using BitString.card_mul_le_two_pow_of_dotProduct_eq S T z h + +/-- The inner product is `1` on `(4^v - 2^v)/2` pairs. -/ +private theorem two_mul_card_dotProduct_eq_true_add_two_pow : + 2 * #{q : BitString v × BitString v | q.1 ⬝ᵥ q.2 = true} + 2 ^ v = 2 ^ v * 2 ^ v := by + simpa using BitString.two_mul_card_dotProduct_eq_true_add_two_pow (ι := Fin v) + +/-- The inner product is `1` or `0` on all `4^v` pairs. -/ +private theorem card_dotProduct_eq_true_add_card_dotProduct_eq_false : + #{q : BitString v × BitString v | q.1 ⬝ᵥ q.2 = true} + + #{q : BitString v × BitString v | q.1 ⬝ᵥ q.2 = false} = 2 ^ v * 2 ^ v := by + have := card_filter_add_card_filter_not (s := univ) + fun q : BitString v × BitString v => q.1 ⬝ᵥ q.2 = true + simpa [Fintype.card_fun, BitString] using this + +/-- `N¹(IP_v) ≥ v - 1`: for `v ≥ 2`, more than `2^(v-2)` rectangles are needed, and for `v ≤ 1` +the bound is `0`. -/ +theorem le_ecomplexityFun_true_dotProduct (v : ℕ) : + ((v - 1 : ℕ) : ℕ∞) ≤ + ecomplexityFun true (fun x y : BitString v => x ⬝ᵥ y) Set.univ Set.univ := by + rcases Nat.lt_or_ge v 2 with hv | hv + · simp [show v - 1 = 0 by omega] + refine le_ecomplexityFun_iff.mpr fun k hk => ?_ + have hT := hk.card_dotProduct_le + have hcount := two_mul_card_dotProduct_eq_true_add_two_pow (v := v) + norm_cast + by_contra! hlt + have hk4 : 2 ^ k * 4 ≤ 2 ^ v := by + rw [show 2 ^ k * 4 = 2 ^ (k + 2) by ring] + exact Nat.pow_le_pow_right (by norm_num) (by omega) + have hN : 4 ≤ 2 ^ v := (Nat.pow_le_pow_right (by norm_num) hv : 2 ^ 2 ≤ 2 ^ v) + nlinarith + +/-- `N⁰(IP_v) ≥ v`: more than `2^(v-1)` rectangles are needed. -/ +theorem le_ecomplexityFun_false_dotProduct (v : ℕ) : + (v : ℕ∞) ≤ ecomplexityFun false (fun x y : BitString v => x ⬝ᵥ y) Set.univ Set.univ := by + refine le_ecomplexityFun_iff.mpr fun k hk => ?_ + have hF := hk.card_dotProduct_le + have hcount := two_mul_card_dotProduct_eq_true_add_two_pow (v := v) + have hsum := card_dotProduct_eq_true_add_card_dotProduct_eq_false (v := v) + norm_cast + by_contra! hlt + have hk2 : 2 ^ k * 2 ≤ 2 ^ v := by + rw [← pow_succ] + exact Nat.pow_le_pow_right (by norm_num) hlt + have hN : 0 < 2 ^ v := by positivity + nlinarith + +end Nondeterministic + +end Cslib.Communication diff --git a/ComplexityTests/NondeterministicFunctions.lean b/ComplexityTests/NondeterministicFunctions.lean new file mode 100644 index 000000000..33f0a9ee5 --- /dev/null +++ b/ComplexityTests/NondeterministicFunctions.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2026 András Z. Salamon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: András Z. Salamon +-/ + +import Complexity.Computability.Communication.Nondeterministic.Functions + +/-! Tests for the nondeterministic complexity of the standard functions: `N⁰(IP_1) = 1`, from the +lower bound and the cover of the zeros of `x₀ ∧ y₀` by two rectangles; the bound `N¹(IP_v) ≥ v - 1` +at `v = 2`, the smallest case where it is positive; and deterministic lower bounds for equality, +disjointness and inner product obtained through `ecomplexityFun_le_protocol`. -/ + +namespace ComplexityTests.NondeterministicFunctions + +open Cslib Cslib.Communication Cslib.Communication.Nondeterministic + +-- `N⁰(IP_1) = 1`: the zeros of `x₀ ∧ y₀` are covered by `{x₀ = 0} × univ` and `univ × {y₀ = 0}`. +example : ecomplexityFun false (fun x y : BitString 1 => x ⬝ᵥ y) Set.univ Set.univ = 1 := by + refine le_antisymm (ecomplexityFun_le_iff.mpr ?_) (le_ecomplexityFun_false_dotProduct 1) + refine ⟨fun w => if w 0 then ({x | x 0 = false}, Set.univ) else (Set.univ, {y | y 0 = false}), + isCover_fun_iff.mpr ⟨fun w x _ hx y _ hy => ?_, fun x _ y _ h => ?_⟩⟩ + · cases hw : w 0 <;> simp only [hw, ite_true, ite_false, Bool.false_eq_true, Set.mem_ofPred_eq, + Set.mem_univ] at hx hy <;> simp [dotProduct, Bool.mul_eq_and, hx, hy] + · cases hx : x 0 + · exact ⟨fun _ => true, by simp [hx], trivial⟩ + · refine ⟨fun _ => false, trivial, ?_⟩ + simpa [dotProduct, Bool.mul_eq_and, hx] using h + +-- `N¹(IP_v) ≥ v - 1` is positive from `v = 2` on. +example : (1 : ℕ∞) ≤ ecomplexityFun true (fun x y : BitString 2 => x ⬝ᵥ y) Set.univ Set.univ := + le_ecomplexityFun_true_dotProduct 2 + +-- Deterministic lower bounds follow, since a protocol gives a cover. +example (v : ℕ) : + (v : ℕ∞) ≤ Protocol.ecomplexityFun (equality : BitString v → BitString v → Bool) := + (ecomplexityFun_equality v).ge.trans (ecomplexityFun_le_protocol true) + +example (v : ℕ) : + (v : ℕ∞) ≤ Protocol.ecomplexityFun (disjointness : BitString v → BitString v → Bool) := + (ecomplexityFun_disjointness v).ge.trans (ecomplexityFun_le_protocol true) + +example (v : ℕ) : (v : ℕ∞) ≤ Protocol.ecomplexityFun fun x y : BitString v => x ⬝ᵥ y := + (le_ecomplexityFun_false_dotProduct v).trans (ecomplexityFun_le_protocol false) + +end ComplexityTests.NondeterministicFunctions From bfb161a8135cf6d1e0f59e96528c6673b8af1461 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:04:05 +0000 Subject: [PATCH 03/23] =?UTF-8?q?doc(communication):=20cite=20Kushilevitz?= =?UTF-8?q?=E2=80=93Nisan=20Definition=202.3=20and=20explain=20the=20round?= =?UTF-8?q?ing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 25 ++++++++++--------- 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index dc4555bf4..4b1c7bde7 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -15,20 +15,21 @@ public import Complexity.Foundations.Data.BitString.Basic # Nondeterministic communication complexity Nondeterministic communication complexity for the answer `z : Bool` is defined by covers -[Kushilevitz and Nisan, Chapter 2][KushilevitzNisan1997]. For a relation `R : X → Y → Bool → Prop`, -a *`z`-cover* of `R` on `A × B` by `2 ^ k` rectangles is a family of rectangles indexed by the -`k`-bit guesses such that `z` is an acceptable answer on the part of each rectangle inside `A × B`, -and every pair of `A × B` on which `!z` is not acceptable lies in some rectangle -(`Nondeterministic.IsCover`). The complexity `Nondeterministic.ecomplexity z R A B` is the least -such `k`, or `⊤` if there is none; in particular it is `⊤` if no answer is acceptable on some pair -of `A × B`, as for `Protocol.ecomplexity`. For a function `f : X → Y → Bool`, +[Kushilevitz and Nisan, Definition 2.3][KushilevitzNisan1997]. For a relation +`R : X → Y → Bool → Prop`, a *`z`-cover* of `R` on `A × B` by `2 ^ k` rectangles is a family of +rectangles indexed by the `k`-bit guesses such that `z` is an acceptable answer on the part of each +rectangle inside `A × B`, and every pair of `A × B` on which `!z` is not acceptable lies in some +rectangle (`Nondeterministic.IsCover`). The complexity `Nondeterministic.ecomplexity z R A B` is the +least such `k`, or `⊤` if there is none; in particular it is `⊤` if no answer is acceptable on some +pair of `A × B`, as for `Protocol.ecomplexity`. For a function `f : X → Y → Bool`, `Nondeterministic.ecomplexityFun z f A B` is the complexity of the relation `f x y = b`; its `z`-covers are families of rectangles on which `f` is `z` inside `A × B` that contain every pair of -`A × B` on which `f` is `z` -(`Nondeterministic.isCover_fun_iff`). Thus `ecomplexityFun true f` and `ecomplexityFun false f` are -`⌈log₂ C^z(f)⌉`, where `C^z(f)` is the least number of rectangles in a `z`-cover (and `0` when `f` -never takes the value `z` on `A × B`): `N¹` and `N⁰` in the cover (certificate) definition, rounded -up to an integer. +`A × B` on which `f` is `z` (`Nondeterministic.isCover_fun_iff`). Thus `ecomplexityFun true f` and +`ecomplexityFun false f` are `⌈log₂ C^z(f)⌉`, where `C^z(f)` is the least number of rectangles in a +`z`-cover (and `0` when `f` never takes the value `z` on `A × B`). Kushilevitz and Nisan define +`N^z(f) = log₂ C^z(f)` without rounding, so `ecomplexityFun z f A B` is their `N^z(f)` rounded up to +an integer, and for `n ≥ 1` a lower bound `n ≤ ecomplexityFun z f A B` says +`C^z(f) > 2 ^ (n - 1)`, that is, `N^z(f) > n - 1` in their convention. A partial function is a function together with the sets `A` and `B`: its value outside `A × B` does not matter, and rectangles are not required to lie inside `A × B`. A partial function whose domain From 2a77a4be6a30eb0d8edafde2bb38fcb93f34ad47 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:04:16 +0000 Subject: [PATCH 04/23] doc(communication): the IP cover bounds in the unrounded convention Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Functions.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean index cbbd62b55..ddea2235d 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Functions.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -27,7 +27,9 @@ Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bi * inner product modulo two: `N¹(IP_v) ≥ v - 1` and `N⁰(IP_v) ≥ v`. By Lindsey's lemma a rectangle on which the inner product is constant has at most `2^v` pairs (`BitString.card_mul_le_two_pow_of_dotProduct_eq`), while the inner product is `1` on - `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. + `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So `C¹(IP_v) ≥ (2^v - 1)/2` and + `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of Kushilevitz and Nisan give + `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. ## Main results From 2e0c44319cd1119b76d9d30bf6760357d449cec6 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:21:37 +0000 Subject: [PATCH 05/23] =?UTF-8?q?doc(communication):=20cite=20Kushilevitz?= =?UTF-8?q?=E2=80=93Nisan=20Example=201.23;=20adapt=20to=20the=20generalis?= =?UTF-8?q?ed=20rectangle=20bound?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../Nondeterministic/Functions.lean | 20 +++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean index ddea2235d..e5a228ed9 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Functions.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -22,8 +22,9 @@ Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bi * equality: `N¹(EQ_v) = v`, from the fooling set of diagonal pairs and the cover by diagonal singletons [Kushilevitz and Nisan, Examples 1.21 and 2.5][KushilevitzNisan1997]; -* disjointness: `N¹(DISJ_v) = v`, from the fooling set of complementary pairs and the cover by the - rectangles `{x ⊆ w} × {y ⊆ wᶜ}`, so `N⁰(NDISJ_v) = v` for its negation; +* disjointness: `N¹(DISJ_v) = v`, from the fooling set of complementary pairs + [Kushilevitz and Nisan, Example 1.23][KushilevitzNisan1997] and the cover by the rectangles + `{x ⊆ w} × {y ⊆ wᶜ}`, so `N⁰(NDISJ_v) = v` for its negation; * inner product modulo two: `N¹(IP_v) ≥ v - 1` and `N⁰(IP_v) ≥ v`. By Lindsey's lemma a rectangle on which the inner product is constant has at most `2^v` pairs (`BitString.card_mul_le_two_pow_of_dotProduct_eq`), while the inner product is `1` on @@ -31,6 +32,10 @@ Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bi `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of Kushilevitz and Nisan give `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. +The deterministic `Cslib.Communication.ecomplexityFun_equality` has the same final name as +`Cslib.Communication.Nondeterministic.ecomplexityFun_equality`; with both namespaces open, write +`Nondeterministic.ecomplexityFun_equality` to avoid an ambiguous name. + ## Main results * `Cslib.Communication.Nondeterministic.ecomplexityFun_equality` @@ -103,10 +108,13 @@ theorem ecomplexityFun_not_disjointness (v : ℕ) : /-- A `z`-cover of the inner product by `2 ^ k` rectangles covers at most `2 ^ k * 2 ^ v` pairs. -/ theorem HasCover.card_dotProduct_le {k : ℕ} {z : Bool} - (hk : HasCover (fun (x y : BitString v) b => x ⬝ᵥ y = b) z Set.univ Set.univ k) : - #{q : BitString v × BitString v | q.1 ⬝ᵥ q.2 = z} ≤ 2 ^ k * 2 ^ v := - hk.card_le_two_pow_mul fun S T h => by - simpa using BitString.card_mul_le_two_pow_of_dotProduct_eq S T z h + (hk : HasCover z (fun (x y : BitString v) b => x ⬝ᵥ y = b) Set.univ Set.univ k) : + #{q : BitString v × BitString v | q.1 ⬝ᵥ q.2 = z} ≤ 2 ^ k * 2 ^ v := by + have h : #{q ∈ (univ : Finset (BitString v)) ×ˢ univ | q.1 ⬝ᵥ q.2 = z} ≤ 2 ^ k * 2 ^ v := + HasCover.card_le_two_pow_mul + (fun S _ T _ h => by simpa using BitString.card_mul_le_two_pow_of_dotProduct_eq S T z h) + (by simpa only [coe_univ] using hk) + rwa [univ_product_univ] at h /-- The inner product is `1` on `(4^v - 2^v)/2` pairs. -/ private theorem two_mul_card_dotProduct_eq_true_add_two_pow : From d2f69357d3cb2440badd93741e50dbc7915e6713 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:21:37 +0000 Subject: [PATCH 06/23] refactor(communication): review nits for nondeterministic complexity IsCover/HasCover take the answer first, as ecomplexity does; hasCover_of_solves becomes Protocol.Solves.hasCover; the rectangle-size bound holds on any finite domain; @[expose] only on IsCover, HasCover and ecomplexityFun; tests on proper subdomains and for a negated relation. Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 97 ++++++++++--------- .../NondeterministicCommunication.lean | 40 ++++++-- 2 files changed, 84 insertions(+), 53 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index 4b1c7bde7..b058bf6d5 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -75,9 +75,10 @@ such covers directly: `Nondeterministic.ecomplexity_le_protocol`. * `Cslib.Communication.Nondeterministic.HasCover.card_le`, `Cslib.Communication.Nondeterministic.le_ecomplexityFun_of_isFoolingSet`: a fooling set of `2 ^ n` pairs with value `z` forces `n`. -* `Cslib.Communication.Nondeterministic.HasCover.card_le_two_pow_mul`: if every `z`-rectangle has - at most `K` pairs, then a `z`-cover by `2 ^ k` rectangles covers at most `2 ^ k * K` pairs. -* `Cslib.Communication.Nondeterministic.hasCover_of_solves`, +* `Cslib.Communication.Nondeterministic.HasCover.card_le_two_pow_mul`: on a finite domain, if every + `z`-rectangle has at most `K` pairs, then a `z`-cover by `2 ^ k` rectangles covers at most + `2 ^ k * K` pairs. +* `Cslib.Communication.Protocol.Solves.hasCover`, `Cslib.Communication.Nondeterministic.ecomplexity_le_protocol`, `Cslib.Communication.Nondeterministic.ecomplexityFun_le_protocol`: nondeterministic complexity is at most deterministic complexity. @@ -87,7 +88,7 @@ such covers directly: `Nondeterministic.ecomplexity_le_protocol`. * [E. Kushilevitz, N. Nisan, *Communication Complexity*][KushilevitzNisan1997] -/ -@[expose] public section +public section namespace Cslib.Communication @@ -100,24 +101,26 @@ variable {X Y : Type*} /-- `C` is a `z`-cover of the relation `R` on `A × B` by `2 ^ k` rectangles: `z` is an acceptable answer on the part of each rectangle inside `A × B`, and every pair of `A × B` on which `!z` is not acceptable lies in some rectangle. -/ -def IsCover (R : X → Y → Bool → Prop) (z : Bool) (A : Set X) (B : Set Y) {k : ℕ} +@[expose] def IsCover (z : Bool) (R : X → Y → Bool → Prop) (A : Set X) (B : Set Y) {k : ℕ} (C : BitString k → Set X × Set Y) : Prop := (∀ w, ∀ x ∈ A, x ∈ (C w).1 → ∀ y ∈ B, y ∈ (C w).2 → R x y z) ∧ ∀ x ∈ A, ∀ y ∈ B, ¬R x y (!z) → ∃ w, x ∈ (C w).1 ∧ y ∈ (C w).2 /-- The relation `R` has a `z`-cover on `A × B` by `2 ^ k` rectangles. -/ -def HasCover (R : X → Y → Bool → Prop) (z : Bool) (A : Set X) (B : Set Y) (k : ℕ) : Prop := - ∃ C : BitString k → Set X × Set Y, IsCover R z A B C +@[expose] def HasCover (z : Bool) (R : X → Y → Bool → Prop) (A : Set X) (B : Set Y) (k : ℕ) : + Prop := + ∃ C : BitString k → Set X × Set Y, IsCover z R A B C /-- The nondeterministic communication complexity of the relation `R` on `A × B` for the answer `z`: the least `k` such that `R` has a `z`-cover on `A × B` by `2 ^ k` rectangles, or `⊤` if there is none. -/ noncomputable def ecomplexity (z : Bool) (R : X → Y → Bool → Prop) (A : Set X) (B : Set Y) : ℕ∞ := - ⨅ k : {k : ℕ // HasCover R z A B k}, (k.1 : ℕ∞) + ⨅ k : {k : ℕ // HasCover z R A B k}, (k.1 : ℕ∞) /-- The nondeterministic communication complexity of `f` on `A × B` for the value `z`: `ecomplexity` of the relation `f x y = b`. `N¹` is `z = true`, and `N⁰` is `z = false`. -/ -noncomputable def ecomplexityFun (z : Bool) (f : X → Y → Bool) (A : Set X) (B : Set Y) : ℕ∞ := +@[expose] noncomputable def ecomplexityFun (z : Bool) (f : X → Y → Bool) (A : Set X) (B : Set Y) : + ℕ∞ := ecomplexity z (fun x y b => f x y = b) A B variable {R R' : X → Y → Bool → Prop} {f : X → Y → Bool} {z : Bool} {A A' : Set X} {B B' : Set Y} @@ -126,7 +129,7 @@ variable {R R' : X → Y → Bool → Prop} {f : X → Y → Bool} {z : Bool} {A /-- A `z`-cover of a function: `f` is `z` on the part of each rectangle inside `A × B`, and every pair of `A × B` on which `f` is `z` lies in some rectangle. -/ theorem isCover_fun_iff {C : BitString k → Set X × Set Y} : - IsCover (fun x y b => f x y = b) z A B C ↔ + IsCover z (fun x y b => f x y = b) A B C ↔ (∀ w, ∀ x ∈ A, x ∈ (C w).1 → ∀ y ∈ B, y ∈ (C w).2 → f x y = z) ∧ ∀ x ∈ A, ∀ y ∈ B, f x y = z → ∃ w, x ∈ (C w).1 ∧ y ∈ (C w).2 := by simp only [IsCover, Bool.eq_not, not_not] @@ -134,12 +137,12 @@ theorem isCover_fun_iff {C : BitString k → Set X × Set Y} : /-! ### Upper and lower bounds -/ /-- A cover by `2 ^ k` rectangles bounds the complexity by `k`. -/ -theorem HasCover.ecomplexity_le (h : HasCover R z A B k) : ecomplexity z R A B ≤ k := - iInf_le (fun k : {k : ℕ // HasCover R z A B k} => (k.1 : ℕ∞)) ⟨k, h⟩ +theorem HasCover.ecomplexity_le (h : HasCover z R A B k) : ecomplexity z R A B ≤ k := + iInf_le (fun k : {k : ℕ // HasCover z R A B k} => (k.1 : ℕ∞)) ⟨k, h⟩ /-- A cover by `2 ^ j` rectangles gives one by `2 ^ k` rectangles for `j ≤ k`: ignore the extra guessed bits. -/ -theorem HasCover.mono_bits (hjk : j ≤ k) (h : HasCover R z A B j) : HasCover R z A B k := by +theorem HasCover.mono_bits (hjk : j ≤ k) (h : HasCover z R A B j) : HasCover z R A B k := by obtain ⟨C, hmem, hcov⟩ := h refine ⟨fun w => C fun i => w (Fin.castLE hjk i), fun w => hmem _, fun x hx y hy hR => ?_⟩ obtain ⟨w, hw⟩ := hcov x hx y hy hR @@ -149,42 +152,42 @@ theorem HasCover.mono_bits (hjk : j ≤ k) (h : HasCover R z A B j) : HasCover R /-- Lower bounds on nondeterministic complexity are lower bounds on the number of guessed bits of every cover. -/ theorem le_ecomplexity_iff {c : ℕ∞} : - c ≤ ecomplexity z R A B ↔ ∀ k, HasCover R z A B k → c ≤ k := by + c ≤ ecomplexity z R A B ↔ ∀ k, HasCover z R A B k → c ≤ k := by simp [ecomplexity, le_iInf_iff, Subtype.forall] /-- `R` has nondeterministic complexity at most `k` exactly when it has a `z`-cover by `2 ^ k` rectangles. -/ -theorem ecomplexity_le_iff : ecomplexity z R A B ≤ k ↔ HasCover R z A B k := by +theorem ecomplexity_le_iff : ecomplexity z R A B ≤ k ↔ HasCover z R A B k := by refine ⟨fun h => ?_, HasCover.ecomplexity_le⟩ - have : Nonempty {k : ℕ // HasCover R z A B k} := by + have : Nonempty {k : ℕ // HasCover z R A B k} := by rw [← ENat.iInf_natCast_ne_top] exact ne_top_of_le_ne_top (ENat.natCast_ne_top k) h obtain ⟨⟨j, hj⟩, hmin⟩ := ENat.exists_eq_iInf - (fun k : {k : ℕ // HasCover R z A B k} => (k.1 : ℕ∞)) + (fun k : {k : ℕ // HasCover z R A B k} => (k.1 : ℕ∞)) exact hj.mono_bits (by exact_mod_cast (hmin.trans_le h : (j : ℕ∞) ≤ k)) /-- `ecomplexity_le_iff` for functions. -/ theorem ecomplexityFun_le_iff : - ecomplexityFun z f A B ≤ k ↔ HasCover (fun x y b => f x y = b) z A B k := + ecomplexityFun z f A B ≤ k ↔ HasCover z (fun x y b => f x y = b) A B k := ecomplexity_le_iff /-- `le_ecomplexity_iff` for functions. -/ theorem le_ecomplexityFun_iff {c : ℕ∞} : - c ≤ ecomplexityFun z f A B ↔ ∀ k, HasCover (fun x y b => f x y = b) z A B k → c ≤ k := + c ≤ ecomplexityFun z f A B ↔ ∀ k, HasCover z (fun x y b => f x y = b) A B k → c ≤ k := le_ecomplexity_iff /-! ### Monotonicity -/ /-- A cover on `A × B` is a cover on any smaller domain. -/ -theorem HasCover.mono (hA : A' ⊆ A) (hB : B' ⊆ B) (h : HasCover R z A B k) : - HasCover R z A' B' k := by +theorem HasCover.mono (hA : A' ⊆ A) (hB : B' ⊆ B) (h : HasCover z R A B k) : + HasCover z R A' B' k := by obtain ⟨C, hmem, hcov⟩ := h exact ⟨C, fun w x hx hxC y hy hyC => hmem w x (hA hx) hxC y (hB hy) hyC, fun x hx y hy hR => hcov x (hA hx) y (hB hy) hR⟩ /-- A cover of `R` is a cover of every weaker relation. -/ -theorem HasCover.of_imp (hR : ∀ x y b, R x y b → R' x y b) (h : HasCover R z A B k) : - HasCover R' z A B k := by +theorem HasCover.of_imp (hR : ∀ x y b, R x y b → R' x y b) (h : HasCover z R A B k) : + HasCover z R' A B k := by obtain ⟨C, hmem, hcov⟩ := h exact ⟨C, fun w x hx hxC y hy hyC => hR x y z (hmem w x hx hxC y hy hyC), fun x hx y hy hR' => hcov x hx y hy fun h => hR' (hR x y _ h)⟩ @@ -209,7 +212,7 @@ theorem ecomplexity_le_of_imp (hR : ∀ x y b, R x y b → R' x y b) : /-- Exchanging the answers exchanges `N⁰` and `N¹`. -/ theorem ecomplexity_not : ecomplexity z (fun x y b => R x y (!b)) A B = ecomplexity (!z) R A B := by - have hiff : ∀ k, HasCover (fun x y b => R x y (!b)) z A B k ↔ HasCover R (!z) A B k := fun k => by + have hiff : ∀ k, HasCover z (fun x y b => R x y (!b)) A B k ↔ HasCover (!z) R A B k := fun k => by simp only [HasCover, IsCover, Bool.not_not] exact le_antisymm (le_ecomplexity_iff.mpr fun k hk => ((hiff k).mpr hk).ecomplexity_le) (le_ecomplexity_iff.mpr fun k hk => ((hiff k).mp hk).ecomplexity_le) @@ -226,7 +229,7 @@ theorem ecomplexity_not : has at most `2 ^ k` pairs if `f` has a `z`-cover on `A × B` by `2 ^ k` rectangles: no rectangle contains two of its pairs. -/ theorem HasCover.card_le {S : Finset (X × Y)} (hS : IsFoolingSet f z S) - (hSAB : ∀ q ∈ S, q.1 ∈ A ∧ q.2 ∈ B) (h : HasCover (fun x y b => f x y = b) z A B k) : + (hSAB : ∀ q ∈ S, q.1 ∈ A ∧ q.2 ∈ B) (h : HasCover z (fun x y b => f x y = b) A B k) : #S ≤ 2 ^ k := by classical obtain ⟨C, hC⟩ := h @@ -253,40 +256,42 @@ theorem le_ecomplexityFun_of_isFoolingSet {S : Finset (X × Y)} (hS : IsFoolingS have := hn.trans (hk.card_le hS hSAB) exact_mod_cast (Nat.pow_le_pow_iff_right (by norm_num)).mp this -/-- **The rectangle-size bound.** If `f` is `z` on at most `K` pairs of every rectangle on which it -is constantly `z`, then a `z`-cover by `2 ^ k` rectangles covers at most `2 ^ k * K` pairs. -/ -theorem HasCover.card_le_two_pow_mul [Fintype X] [Fintype Y] {K : ℕ} - (hK : ∀ (S : Finset X) (T : Finset Y), (∀ x ∈ S, ∀ y ∈ T, f x y = z) → #S * #T ≤ K) - (h : HasCover (fun x y b => f x y = b) z Set.univ Set.univ k) : - #{q : X × Y | f q.1 q.2 = z} ≤ 2 ^ k * K := by +/-- **The rectangle-size bound.** Let `s` and `t` be finite. If every rectangle inside `s × t` on +which `f` is constantly `z` has at most `K` pairs, then a `z`-cover of `f` on `s × t` by `2 ^ k` +rectangles covers at most `2 ^ k * K` pairs, so `f` is `z` on at most `2 ^ k * K` pairs of +`s × t`. -/ +theorem HasCover.card_le_two_pow_mul {s : Finset X} {t : Finset Y} {K : ℕ} + (hK : ∀ S ⊆ s, ∀ T ⊆ t, (∀ x ∈ S, ∀ y ∈ T, f x y = z) → #S * #T ≤ K) + (h : HasCover z (fun x y b => f x y = b) s t k) : + #{q ∈ s ×ˢ t | f q.1 q.2 = z} ≤ 2 ^ k * K := by classical obtain ⟨C, hC⟩ := h obtain ⟨hmem, hcov⟩ := isCover_fun_iff.mp hC - let S : BitString k → Finset X := fun w => {x | x ∈ (C w).1} - let T : BitString k → Finset Y := fun w => {y | y ∈ (C w).2} - have hsub : ({q : X × Y | f q.1 q.2 = z} : Finset (X × Y)) ⊆ - univ.biUnion fun w => S w ×ˢ T w := by + let S : BitString k → Finset X := fun w => {x ∈ s | x ∈ (C w).1} + let T : BitString k → Finset Y := fun w => {y ∈ t | y ∈ (C w).2} + have hsub : {q ∈ s ×ˢ t | f q.1 q.2 = z} ⊆ univ.biUnion fun w => S w ×ˢ T w := by intro q hq - simp only [mem_filter, mem_univ, true_and] at hq - obtain ⟨w, hx, hy⟩ := hcov q.1 trivial q.2 trivial hq - simp only [mem_biUnion, mem_univ, true_and, mem_product] - exact ⟨w, by simpa [S] using hx, by simpa [T] using hy⟩ - calc #{q : X × Y | f q.1 q.2 = z} ≤ #(univ.biUnion fun w => S w ×ˢ T w) := card_le_card hsub + simp only [mem_filter, mem_product] at hq + obtain ⟨w, hx, hy⟩ := hcov q.1 hq.1.1 q.2 hq.1.2 hq.2 + simp only [mem_biUnion, mem_univ, true_and, mem_product, mem_filter, S, T] + exact ⟨w, ⟨hq.1.1, hx⟩, hq.1.2, hy⟩ + calc #{q ∈ s ×ˢ t | f q.1 q.2 = z} ≤ #(univ.biUnion fun w => S w ×ˢ T w) := card_le_card hsub _ ≤ ∑ w, #(S w ×ˢ T w) := card_biUnion_le _ ≤ ∑ _w : BitString k, K := by refine sum_le_sum fun w _ => ?_ rw [card_product] - refine hK _ _ fun x hx y hy => hmem w x trivial ?_ y trivial ?_ - · simpa [S] using hx - · simpa [T] using hy + refine hK _ (filter_subset _ _) _ (filter_subset _ _) fun x hx y hy => ?_ + simp only [mem_filter, T] at hx hy + exact hmem w x hx.1 hx.2 y hy.1 hy.2 _ = 2 ^ k * K := by rw [sum_const, card_univ, BitString.card, smul_eq_mul] /-! ### Comparison with deterministic complexity -/ /-- The leaves with output `z` of a deterministic protocol solving `R` on `A × B` form a `z`-cover of `R` by `2 ^ depth` rectangles. -/ -theorem hasCover_of_solves {p : Protocol X Y Bool} (hp : p.Solves R A B) (z : Bool) : - HasCover R z A B p.depth := by +theorem _root_.Cslib.Communication.Protocol.Solves.hasCover {p : Protocol X Y Bool} + (hp : p.Solves R A B) (z : Bool) : + HasCover z R A B p.depth := by classical let e := BitString.equivFin p.depth refine ⟨fun w => if h : (e w : ℕ) < p.leafCount then @@ -312,7 +317,7 @@ theorem hasCover_of_solves {p : Protocol X Y Bool} (hp : p.Solves R A B) (z : Bo /-- **Nondeterministic complexity is at most deterministic complexity.** -/ theorem ecomplexity_le_protocol (z : Bool) : ecomplexity z R A B ≤ Protocol.ecomplexity R A B := - le_iInf fun p => (hasCover_of_solves p.2 z).ecomplexity_le + le_iInf fun p => (p.2.hasCover z).ecomplexity_le /-- `ecomplexity_le_protocol` for functions on all inputs. -/ theorem ecomplexityFun_le_protocol (z : Bool) : diff --git a/ComplexityTests/NondeterministicCommunication.lean b/ComplexityTests/NondeterministicCommunication.lean index 42d98fe9f..27b4af61e 100644 --- a/ComplexityTests/NondeterministicCommunication.lean +++ b/ComplexityTests/NondeterministicCommunication.lean @@ -10,8 +10,9 @@ import Complexity.Computability.Communication.Nondeterministic.Basic /-! Tests for nondeterministic communication complexity by covers: exact values for equality on three values (`N¹ = 2 = ⌈log₂ 3⌉`, by an explicit cover and the rectangle-size bound) and on `Bool` (`N⁰ = 1`, by an explicit cover and a fooling set, and `N¹` of inequality by negation); smaller -domains that make equality trivial; a relation with several acceptable answers, which is easier -than the function it relaxes, and one with none, which has no cover; and bounds by deterministic +domains that make equality trivial, and the fooling-set and rectangle-size bounds on a proper +subdomain; a relation with several acceptable answers, which is easier than the function it relaxes, +with its answers exchanged, and one with none, which has no cover; and bounds by deterministic protocols, for a function and for a relation. -/ namespace ComplexityTests.NondeterministicCommunication @@ -38,8 +39,10 @@ example : ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) Set.univ Set · intro x _ y _ h simp only [equality, decide_eq_true_eq] at h exact ⟨e.symm ⟨x, by omega⟩, by simp, by simp [h]⟩ - · have := hk.card_le_two_pow_mul card_mul_le_one_of_equality - have h3 : #{q : Fin 3 × Fin 3 | equality q.1 q.2 = true} = 3 := by decide + · have : #{q ∈ (univ : Finset (Fin 3)) ×ˢ univ | equality q.1 q.2 = true} ≤ 2 ^ k * 1 := + HasCover.card_le_two_pow_mul (fun S _ T _ h => card_mul_le_one_of_equality S T h) + (by simpa only [coe_univ] using hk) + have h3 : #{q ∈ (univ : Finset (Fin 3)) ×ˢ univ | equality q.1 q.2 = true} = 3 := by decide rw [h3, mul_one] at this have : 2 ≤ k := by by_contra! hk @@ -58,6 +61,25 @@ example : ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) {0} {0, 1} = nonpos_iff_eq_zero.mp <| (ecomplexityFun_mono le_rfl (Set.subset_univ _)).trans ecomplexityFun_equality_zero_univ.le +-- On `{0, 1} × {0, 1}` the fooling set `{(0, 0), (1, 1)}` lies inside the domain, so `N¹ ≥ 1`. +example : (1 : ℕ∞) ≤ ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) {0, 1} {0, 1} := + le_ecomplexityFun_of_isFoolingSet (isFoolingSet_equality {0, 1}) (by decide) (by decide) + +-- The rectangle-size bound on the finite domain `{0, 1} × {0, 1}`: two diagonal pairs and one pair +-- per rectangle need two rectangles. +example : (1 : ℕ∞) ≤ ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) {0, 1} {0, 1} := by + refine le_ecomplexityFun_iff.mpr fun k hk => ?_ + have : #{q ∈ ({0, 1} : Finset (Fin 3)) ×ˢ {0, 1} | equality q.1 q.2 = true} ≤ 2 ^ k * 1 := + HasCover.card_le_two_pow_mul (fun S _ T _ h => card_mul_le_one_of_equality S T h) + (by simpa only [coe_insert, coe_singleton] using hk) + have h2 : #{q ∈ ({0, 1} : Finset (Fin 3)) ×ˢ {0, 1} | equality q.1 q.2 = true} = 2 := by decide + rw [h2, mul_one] at this + have : 1 ≤ k := by + by_contra! hk + interval_cases k + simp at this + exact_mod_cast this + /-! ### Equality on `Bool` -/ /-- `N⁰(EQ)` on `Bool` is `1`: `(false, true)` and `(true, false)` form a fooling set with value @@ -88,12 +110,16 @@ example : ecomplexityFun true (fun x y : Bool => !equality x y) Set.univ Set.uni /-- Equality under the promise `x = y`: off the diagonal every answer is acceptable. -/ private def promiseEq (x y : Bool) (b : Bool) : Prop := x = y → b = true --- No pair must be covered with `false`, since `true` is acceptable everywhere: one empty --- rectangle is a `0`-cover, although `N⁰` of equality itself is `1`. -example : ecomplexity false promiseEq Set.univ Set.univ = 0 := +/-- No pair must be covered with `false`, since `true` is acceptable everywhere: one empty +rectangle is a `0`-cover, although `N⁰` of equality itself is `1`. -/ +private theorem ecomplexity_false_promiseEq : ecomplexity false promiseEq Set.univ Set.univ = 0 := nonpos_iff_eq_zero.mp <| ecomplexity_le_iff.mpr ⟨fun _ => (∅, ∅), fun _ _ _ hx => hx.elim, fun _ _ _ _ h => (h fun _ => rfl).elim⟩ +-- Exchanging the answers of the relation exchanges `N⁰` and `N¹`. +example : ecomplexity true (fun x y b => promiseEq x y (!b)) Set.univ Set.univ = 0 := by + rw [ecomplexity_not, Bool.not_true, ecomplexity_false_promiseEq] + -- The relation is weaker than equality, so it is no harder. example : ecomplexity false promiseEq Set.univ Set.univ ≤ ecomplexityFun false (equality : Bool → Bool → Bool) Set.univ Set.univ := From db63b2c84c610db66e6f022f33e8b8b2533f069a Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:30:46 +0000 Subject: [PATCH 07/23] =?UTF-8?q?doc(communication):=20cite=20Kushilevitz?= =?UTF-8?q?=E2=80=93Nisan=20Example=201.25=20for=20the=20inner=20product?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../Nondeterministic/Functions.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean index e5a228ed9..37975ca98 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Functions.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -17,20 +17,20 @@ public import Complexity.Computability.Communication.Nondeterministic.Basic /-! # Nondeterministic complexity of equality, disjointness and inner product -Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bit strings -[Kushilevitz and Nisan, Chapters 1–3][KushilevitzNisan1997]: +Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bit strings: * equality: `N¹(EQ_v) = v`, from the fooling set of diagonal pairs and the cover by diagonal singletons [Kushilevitz and Nisan, Examples 1.21 and 2.5][KushilevitzNisan1997]; * disjointness: `N¹(DISJ_v) = v`, from the fooling set of complementary pairs [Kushilevitz and Nisan, Example 1.23][KushilevitzNisan1997] and the cover by the rectangles `{x ⊆ w} × {y ⊆ wᶜ}`, so `N⁰(NDISJ_v) = v` for its negation; -* inner product modulo two: `N¹(IP_v) ≥ v - 1` and `N⁰(IP_v) ≥ v`. By Lindsey's - lemma a rectangle on which the inner product is constant has at most `2^v` pairs - (`BitString.card_mul_le_two_pow_of_dotProduct_eq`), while the inner product is `1` on - `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So `C¹(IP_v) ≥ (2^v - 1)/2` and - `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of Kushilevitz and Nisan give - `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. +* inner product modulo two: `N¹(IP_v) ≥ v - 1` and `N⁰(IP_v) ≥ v`. A rectangle on which the inner + product is constant has at most `2^v` pairs: for the value `0` this is + [Kushilevitz and Nisan, Example 1.25][KushilevitzNisan1997], and for both values it follows from + Lindsey's lemma (`BitString.card_mul_le_two_pow_of_dotProduct_eq`). Meanwhile the inner product is + `1` on `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So `C¹(IP_v) ≥ (2^v - 1)/2` and + `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of Kushilevitz and Nisan give, for + `v ≥ 1`, `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. The deterministic `Cslib.Communication.ecomplexityFun_equality` has the same final name as `Cslib.Communication.Nondeterministic.ecomplexityFun_equality`; with both namespaces open, write From 29e3cd33a37be3c9e9045c8f53b7e453eb7ecf70 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:34:21 +0000 Subject: [PATCH 08/23] =?UTF-8?q?doc(communication):=20cite=20Kushilevitz?= =?UTF-8?q?=E2=80=93Nisan=20only=20for=20the=20lower=20bound=20on=20equali?= =?UTF-8?q?ty?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Functions.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean index 37975ca98..94b0888ce 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Functions.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -19,8 +19,9 @@ public import Complexity.Computability.Communication.Nondeterministic.Basic Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bit strings: -* equality: `N¹(EQ_v) = v`, from the fooling set of diagonal pairs and the cover by diagonal - singletons [Kushilevitz and Nisan, Examples 1.21 and 2.5][KushilevitzNisan1997]; +* equality: `N¹(EQ_v) = v`, from the fooling set of diagonal pairs + [Kushilevitz and Nisan, Examples 1.21 and 2.5][KushilevitzNisan1997] and, for the upper bound, + the cover by the `2^v` diagonal singletons; * disjointness: `N¹(DISJ_v) = v`, from the fooling set of complementary pairs [Kushilevitz and Nisan, Example 1.23][KushilevitzNisan1997] and the cover by the rectangles `{x ⊆ w} × {y ⊆ wᶜ}`, so `N⁰(NDISJ_v) = v` for its negation; From 4093e23da37d5f2548b5bc5f736ea13a4b5e8c5d Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:35:42 +0000 Subject: [PATCH 09/23] =?UTF-8?q?doc(communication):=20Kushilevitz?= =?UTF-8?q?=E2=80=93Nisan=20Example=202.5=20states=20N=C2=B9(EQ)=20=3D=20n?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Functions.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean index 94b0888ce..ee4c7e225 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Functions.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -19,8 +19,8 @@ public import Complexity.Computability.Communication.Nondeterministic.Basic Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bit strings: -* equality: `N¹(EQ_v) = v`, from the fooling set of diagonal pairs - [Kushilevitz and Nisan, Examples 1.21 and 2.5][KushilevitzNisan1997] and, for the upper bound, +* equality: `N¹(EQ_v) = v` [Kushilevitz and Nisan, Example 2.5][KushilevitzNisan1997], where the + lower bound is the fooling set of diagonal pairs of their Example 1.21; the upper bound here is the cover by the `2^v` diagonal singletons; * disjointness: `N¹(DISJ_v) = v`, from the fooling set of complementary pairs [Kushilevitz and Nisan, Example 1.23][KushilevitzNisan1997] and the cover by the rectangles From 9b5d8065ccbdccac61f61b6c6f7520cacad6f867 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:56:30 +0000 Subject: [PATCH 10/23] doc(communication): state the protocol conventions precisely Covers spend no bits on the answer; with both players learning it, as in Protocol, a cover by 2^k rectangles gives a protocol of cost k + 2 (k + 1 if one player suffices). Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 26 ++++++++++++------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index b058bf6d5..942f16472 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -37,15 +37,23 @@ is not a rectangle is a relation that accepts every answer outside its domain. ## Covers and protocols -A nondeterministic protocol of cost `c` gives a cover by at most `2 ^ c` rectangles, so lower bounds -on `ecomplexity` hold for every protocol convention. Protocol definitions differ from this one by -at most an additive constant, so an upper bound here is slightly weaker than an upper bound for -protocols. Conversely, a cover by `2 ^ k` rectangles gives a protocol: guess `k` bits naming a -rectangle, Alice sends one bit saying whether her input is in its first side, and Bob accepts when -both inputs are in it, for cost `k + 1`, or `k + 2` if Bob's answer is counted as a sent bit. So a -nondeterministic protocol of cost `c` proves `ecomplexity z R A B ≤ c` once it is converted to a -cover by `2 ^ c` rectangles (`Nondeterministic.ecomplexity_le_iff`). Deterministic protocols give -such covers directly: `Nondeterministic.ecomplexity_le_protocol`. +Covers count rectangles; no bits are spent announcing the answer. Protocols must announce it, and +conventions differ on who must learn it. In `Protocol` the answer is a function of the transcript, +so both players know it; for instance, equality on `v`-bit strings has deterministic complexity +`v + 1` for `v ≥ 1` (`Cslib.Communication.ecomplexityFun_equality`). For nondeterministic protocols +in the same convention, where the guessed bits count towards the cost and at the end both players +know whether to accept, the two notions differ by at most two bits: + +* a protocol of cost `c` gives a cover by at most `2 ^ c` rectangles, one for each accepting + transcript, so a lower bound on `ecomplexity` is a lower bound for protocols, whatever the + convention for announcing the answer; +* a cover by `2 ^ k` rectangles gives a protocol of cost `k + 2`: the `k` guessed bits name a + rectangle, and Alice and Bob each send one bit saying whether their input lies in its side. If + only one player needs to learn the answer, Bob need not reply, and the cost is `k + 1`. + +So `ecomplexity z R A B ≤ k` gives a protocol of cost `k + 2`, and a protocol of cost `c`, once +converted to a cover, gives `ecomplexity z R A B ≤ c` (`Nondeterministic.ecomplexity_le_iff`). +Deterministic protocols give covers directly (`Nondeterministic.ecomplexity_le_protocol`). ## Main definitions From 4517ea76d526ac62c6a86b75a145566a7d26e707 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:56:31 +0000 Subject: [PATCH 11/23] =?UTF-8?q?doc(communication):=20compare=20N=C2=B9(E?= =?UTF-8?q?Q)=20with=20D(EQ);=20gloss=20Lindsey's=20lemma?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Functions.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean index ee4c7e225..4616d2dc5 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Functions.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -21,17 +21,19 @@ Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bi * equality: `N¹(EQ_v) = v` [Kushilevitz and Nisan, Example 2.5][KushilevitzNisan1997], where the lower bound is the fooling set of diagonal pairs of their Example 1.21; the upper bound here is - the cover by the `2^v` diagonal singletons; + the cover by the `2^v` diagonal singletons. Deterministically one more bit is needed, to announce + the answer: `Cslib.Communication.ecomplexityFun_equality` gives `v + 1` for `v ≥ 1` (see the + module `Nondeterministic.Basic` on conventions); * disjointness: `N¹(DISJ_v) = v`, from the fooling set of complementary pairs [Kushilevitz and Nisan, Example 1.23][KushilevitzNisan1997] and the cover by the rectangles `{x ⊆ w} × {y ⊆ wᶜ}`, so `N⁰(NDISJ_v) = v` for its negation; * inner product modulo two: `N¹(IP_v) ≥ v - 1` and `N⁰(IP_v) ≥ v`. A rectangle on which the inner product is constant has at most `2^v` pairs: for the value `0` this is [Kushilevitz and Nisan, Example 1.25][KushilevitzNisan1997], and for both values it follows from - Lindsey's lemma (`BitString.card_mul_le_two_pow_of_dotProduct_eq`). Meanwhile the inner product is - `1` on `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So `C¹(IP_v) ≥ (2^v - 1)/2` and - `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of Kushilevitz and Nisan give, for - `v ≥ 1`, `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. + Lindsey's lemma, the Hadamard rectangle bound (`BitString.card_mul_le_two_pow_of_dotProduct_eq`). + Meanwhile the inner product is `1` on `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So + `C¹(IP_v) ≥ (2^v - 1)/2` and `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of + Kushilevitz and Nisan give, for `v ≥ 1`, `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. The deterministic `Cslib.Communication.ecomplexityFun_equality` has the same final name as `Cslib.Communication.Nondeterministic.ecomplexityFun_equality`; with both namespaces open, write From 7b1b874fd31d73b78c67e15fce8dccd6dbb867e0 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:58:30 +0000 Subject: [PATCH 12/23] doc(communication): cite Jukna for Lindsey's lemma Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Functions.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean index 4616d2dc5..ee9f23592 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Functions.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -30,10 +30,11 @@ Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bi * inner product modulo two: `N¹(IP_v) ≥ v - 1` and `N⁰(IP_v) ≥ v`. A rectangle on which the inner product is constant has at most `2^v` pairs: for the value `0` this is [Kushilevitz and Nisan, Example 1.25][KushilevitzNisan1997], and for both values it follows from - Lindsey's lemma, the Hadamard rectangle bound (`BitString.card_mul_le_two_pow_of_dotProduct_eq`). - Meanwhile the inner product is `1` on `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So - `C¹(IP_v) ≥ (2^v - 1)/2` and `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of - Kushilevitz and Nisan give, for `v ≥ 1`, `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. + Lindsey's lemma, stated for Hadamard matrices in [Jukna, Appendix A, p. 579][Jukna2012] + (`BitString.card_mul_le_two_pow_of_dotProduct_eq`). Meanwhile the inner product is `1` on + `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So `C¹(IP_v) ≥ (2^v - 1)/2` and + `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of Kushilevitz and Nisan give, for + `v ≥ 1`, `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. The deterministic `Cslib.Communication.ecomplexityFun_equality` has the same final name as `Cslib.Communication.Nondeterministic.ecomplexityFun_equality`; with both namespaces open, write @@ -50,6 +51,7 @@ The deterministic `Cslib.Communication.ecomplexityFun_equality` has the same fin ## References +* [S. Jukna, *Boolean Function Complexity: Advances and Frontiers*][Jukna2012] * [E. Kushilevitz, N. Nisan, *Communication Complexity*][KushilevitzNisan1997] -/ From 058da5337054ceca30155bf7b0d79de092a41c30 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:07:28 +0000 Subject: [PATCH 13/23] doc(communication): explain the inner-product rectangle bound via Lindsey's lemma and over F2 Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Functions.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean index ee9f23592..d09ecbf67 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Functions.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -28,11 +28,15 @@ Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bi [Kushilevitz and Nisan, Example 1.23][KushilevitzNisan1997] and the cover by the rectangles `{x ⊆ w} × {y ⊆ wᶜ}`, so `N⁰(NDISJ_v) = v` for its negation; * inner product modulo two: `N¹(IP_v) ≥ v - 1` and `N⁰(IP_v) ≥ v`. A rectangle on which the inner - product is constant has at most `2^v` pairs: for the value `0` this is - [Kushilevitz and Nisan, Example 1.25][KushilevitzNisan1997], and for both values it follows from - Lindsey's lemma, stated for Hadamard matrices in [Jukna, Appendix A, p. 579][Jukna2012] - (`BitString.card_mul_le_two_pow_of_dotProduct_eq`). Meanwhile the inner product is `1` on - `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So `C¹(IP_v) ≥ (2^v - 1)/2` and + product is constant has at most `2^v` pairs. The matrix `(-1)^(x ⬝ᵥ y)` is a `2^v × 2^v` Hadamard + matrix, and the inner product is constant on a rectangle exactly when this matrix is, so this is + the final statement of Lindsey's lemma [Jukna, Appendix A, p. 579][Jukna2012]: no `a × b` + submatrix of an `n × n` Hadamard matrix with `a b > n` is monochromatic + (`BitString.card_mul_le_two_pow_of_dotProduct_eq`, proved from the bound on signed sums). For the + value `0` it is also [Kushilevitz and Nisan, Example 1.25][KushilevitzNisan1997], by linear + algebra over `𝔽₂`; the value `1` reduces to it by translating the two sides of the rectangle by + one of their elements, after which the inner product is `0` on it. Meanwhile the inner product is + `1` on `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So `C¹(IP_v) ≥ (2^v - 1)/2` and `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of Kushilevitz and Nisan give, for `v ≥ 1`, `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. From 826d908a1b72de90abe656f6031b29476e52813e Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:12:53 +0000 Subject: [PATCH 14/23] doc(communication): mark the formal proof of the inner-product rectangle bound Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Functions.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Functions.lean b/Complexity/Computability/Communication/Nondeterministic/Functions.lean index d09ecbf67..b92d4f890 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Functions.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Functions.lean @@ -32,13 +32,14 @@ Bounds on `Nondeterministic.ecomplexityFun` for the standard functions on `v`-bi matrix, and the inner product is constant on a rectangle exactly when this matrix is, so this is the final statement of Lindsey's lemma [Jukna, Appendix A, p. 579][Jukna2012]: no `a × b` submatrix of an `n × n` Hadamard matrix with `a b > n` is monochromatic - (`BitString.card_mul_le_two_pow_of_dotProduct_eq`, proved from the bound on signed sums). For the - value `0` it is also [Kushilevitz and Nisan, Example 1.25][KushilevitzNisan1997], by linear - algebra over `𝔽₂`; the value `1` reduces to it by translating the two sides of the rectangle by - one of their elements, after which the inner product is `0` on it. Meanwhile the inner product is - `1` on `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So `C¹(IP_v) ≥ (2^v - 1)/2` and - `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of Kushilevitz and Nisan give, for - `v ≥ 1`, `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. + (`BitString.card_mul_le_two_pow_of_dotProduct_eq`; this is the formal proof, via the bound on + signed sums). Alternatively, for the value `0` the bound is + [Kushilevitz and Nisan, Example 1.25][KushilevitzNisan1997], by linear algebra over `𝔽₂`, and the + value `1` reduces to it by translating the two sides of the rectangle by one of their elements, + after which the inner product is `0` on it; this argument is not formalised here. Meanwhile the + inner product is `1` on `(4^v - 2^v)/2` pairs and `0` on `(4^v + 2^v)/2` pairs. So + `C¹(IP_v) ≥ (2^v - 1)/2` and `C⁰(IP_v) ≥ (2^v + 1)/2`, which in the unrounded convention of + Kushilevitz and Nisan give, for `v ≥ 1`, `N¹(IP_v) ≥ log₂ (2^v - 1) - 1` and `N⁰(IP_v) > v - 1`. The deterministic `Cslib.Communication.ecomplexityFun_equality` has the same final name as `Cslib.Communication.Nondeterministic.ecomplexityFun_equality`; with both namespaces open, write From d43f9e9a4ee636d4d811157b03a111f61dbfbac8 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:29:03 +0000 Subject: [PATCH 15/23] =?UTF-8?q?doc(communication):=20locate=20Kushilevit?= =?UTF-8?q?z=E2=80=93Nisan=20Definition=202.3=20and=20separate=20it=20from?= =?UTF-8?q?=20the=20extension?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Their definition is for a Boolean function on all of X × Y; the domain sets and relations are the extension made here. Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 20 ++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index 942f16472..07dc8e5b0 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -15,7 +15,7 @@ public import Complexity.Foundations.Data.BitString.Basic # Nondeterministic communication complexity Nondeterministic communication complexity for the answer `z : Bool` is defined by covers -[Kushilevitz and Nisan, Definition 2.3][KushilevitzNisan1997]. For a relation +[Kushilevitz and Nisan, Definition 2.3, p. 18][KushilevitzNisan1997]. For a relation `R : X → Y → Bool → Prop`, a *`z`-cover* of `R` on `A × B` by `2 ^ k` rectangles is a family of rectangles indexed by the `k`-bit guesses such that `z` is an acceptable answer on the part of each rectangle inside `A × B`, and every pair of `A × B` on which `!z` is not acceptable lies in some @@ -26,14 +26,16 @@ pair of `A × B`, as for `Protocol.ecomplexity`. For a function `f : X → Y → `z`-covers are families of rectangles on which `f` is `z` inside `A × B` that contain every pair of `A × B` on which `f` is `z` (`Nondeterministic.isCover_fun_iff`). Thus `ecomplexityFun true f` and `ecomplexityFun false f` are `⌈log₂ C^z(f)⌉`, where `C^z(f)` is the least number of rectangles in a -`z`-cover (and `0` when `f` never takes the value `z` on `A × B`). Kushilevitz and Nisan define -`N^z(f) = log₂ C^z(f)` without rounding, so `ecomplexityFun z f A B` is their `N^z(f)` rounded up to -an integer, and for `n ≥ 1` a lower bound `n ≤ ecomplexityFun z f A B` says -`C^z(f) > 2 ^ (n - 1)`, that is, `N^z(f) > n - 1` in their convention. - -A partial function is a function together with the sets `A` and `B`: its value outside `A × B` does -not matter, and rectangles are not required to lie inside `A × B`. A partial function whose domain -is not a rectangle is a relation that accepts every answer outside its domain. +`z`-cover (and `0` when `f` never takes the value `z` on `A × B`). + +Kushilevitz and Nisan define `N^z(f) = log₂ C^z(f)` for a Boolean function `f` on all of `X × Y`, +without rounding. So for such `f`, `ecomplexityFun z f Set.univ Set.univ` is their `N^z(f)` rounded +up to an integer, and for `n ≥ 1` a lower bound `n ≤ ecomplexityFun z f Set.univ Set.univ` says +`C^z(f) > 2 ^ (n - 1)`, that is, `N^z(f) > n - 1` in their convention. The domain sets `A` and `B` +and the relations are an extension made here. A partial function is a function together with the +sets `A` and `B`: its value outside `A × B` does not matter, and rectangles are not required to lie +inside `A × B`. A partial function whose domain is not a rectangle is a relation that accepts every +answer outside its domain. ## Covers and protocols From 90fff4b0e2ff6fc7bee3cb0a57c3aad3aca432e2 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:32:56 +0000 Subject: [PATCH 16/23] =?UTF-8?q?doc(communication):=20cite=20Kushilevitz?= =?UTF-8?q?=E2=80=93Nisan=20Definition=202.1(4)=20for=20the=20cover=20numb?= =?UTF-8?q?er?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../Computability/Communication/Nondeterministic/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index 07dc8e5b0..6e3a7dac8 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -26,7 +26,8 @@ pair of `A × B`, as for `Protocol.ecomplexity`. For a function `f : X → Y → `z`-covers are families of rectangles on which `f` is `z` inside `A × B` that contain every pair of `A × B` on which `f` is `z` (`Nondeterministic.isCover_fun_iff`). Thus `ecomplexityFun true f` and `ecomplexityFun false f` are `⌈log₂ C^z(f)⌉`, where `C^z(f)` is the least number of rectangles in a -`z`-cover (and `0` when `f` never takes the value `z` on `A × B`). +`z`-cover [Kushilevitz and Nisan, Definition 2.1(4), p. 17][KushilevitzNisan1997] (and `0` when `f` +never takes the value `z` on `A × B`). Kushilevitz and Nisan define `N^z(f) = log₂ C^z(f)` for a Boolean function `f` on all of `X × Y`, without rounding. So for such `f`, `ecomplexityFun z f Set.univ Set.univ` is their `N^z(f)` rounded From 0ca85e0085bc3974178e59650f557a6a973ec06b Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:38:25 +0000 Subject: [PATCH 17/23] doc(communication): place the partial-function and relation forms relative to the source MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit They extend Definition 2.1 in the usual way for promise problems; relations in general are the subject of Kushilevitz–Nisan Chapter 5. Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index 6e3a7dac8..7a7f84297 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -32,11 +32,16 @@ never takes the value `z` on `A × B`). Kushilevitz and Nisan define `N^z(f) = log₂ C^z(f)` for a Boolean function `f` on all of `X × Y`, without rounding. So for such `f`, `ecomplexityFun z f Set.univ Set.univ` is their `N^z(f)` rounded up to an integer, and for `n ≥ 1` a lower bound `n ≤ ecomplexityFun z f Set.univ Set.univ` says -`C^z(f) > 2 ^ (n - 1)`, that is, `N^z(f) > n - 1` in their convention. The domain sets `A` and `B` -and the relations are an extension made here. A partial function is a function together with the -sets `A` and `B`: its value outside `A × B` does not matter, and rectangles are not required to lie -inside `A × B`. A partial function whose domain is not a rectangle is a relation that accepts every -answer outside its domain. +`C^z(f) > 2 ^ (n - 1)`, that is, `N^z(f) > n - 1` in their convention. + +The domain sets `A` and `B` and the relations go beyond their Definition 2.1, in the usual way for +partial functions (promise problems). A partial function is a function together with the sets `A` +and `B`: its value outside `A × B` does not matter, and rectangles are not required to lie inside +`A × B`. A relation with Boolean answers is a partial function with an arbitrary domain, accepting +both answers outside it, except that it may accept no answer on some pairs, which makes the +complexity `⊤`. Relations with arbitrary answers are the subject of +[Kushilevitz and Nisan, Chapter 5][KushilevitzNisan1997], and `Protocol.ecomplexity` is stated for +them. ## Covers and protocols From 2cc36276f675c502ed47dc66b38efb4874ca9657 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:46:43 +0000 Subject: [PATCH 18/23] =?UTF-8?q?doc(communication):=20compare=20with=20Ku?= =?UTF-8?q?shilevitz=E2=80=93Nisan's=20convention=20for=20illegal=20inputs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Their Definition 5.2 asks for correctness on legal inputs only, and they note the alternative of allowing every answer on illegal pairs; here, as for Protocol.ecomplexity, every pair must be answered, which agrees with theirs on that extension. Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index 7a7f84297..a9f66faf3 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -38,10 +38,18 @@ The domain sets `A` and `B` and the relations go beyond their Definition 2.1, in partial functions (promise problems). A partial function is a function together with the sets `A` and `B`: its value outside `A × B` does not matter, and rectangles are not required to lie inside `A × B`. A relation with Boolean answers is a partial function with an arbitrary domain, accepting -both answers outside it, except that it may accept no answer on some pairs, which makes the -complexity `⊤`. Relations with arbitrary answers are the subject of +both answers outside it, except that it may accept no answer on some pairs. + +Relations with arbitrary answers are the subject of [Kushilevitz and Nisan, Chapter 5][KushilevitzNisan1997], and `Protocol.ecomplexity` is stated for -them. +them. Kushilevitz and Nisan require a protocol to be correct only on legal inputs, those with some +acceptable answer, and define the other measures for relations "in a similar manner" +[Kushilevitz and Nisan, Definition 5.2, p. 71][KushilevitzNisan1997]. Here, as for +`Protocol.ecomplexity`, every pair of `A × B` must get an acceptable answer, so a pair of `A × B` +with no acceptable answer makes the complexity `⊤`. Just before Definition 5.2 they note the +alternative of extending a relation to allow every answer on its illegal pairs; their convention +for `R` is this one for that extension, which is no harder than `R` +(`Nondeterministic.ecomplexity_le_of_imp`). ## Covers and protocols From 0d2293ede451fa7f69a5147a30c94e59c365c353 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:49:55 +0000 Subject: [PATCH 19/23] doc(communication): why the relations have Boolean answers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Kushilevitz–Nisan remark that N¹(R) is less interesting for relations with arbitrary answers; with Boolean answers a relation is a partial Boolean function. Co-Authored-By: Claude Opus 5.5 --- .../Computability/Communication/Nondeterministic/Basic.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index a9f66faf3..5ba7be44d 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -49,7 +49,10 @@ acceptable answer, and define the other measures for relations "in a similar man with no acceptable answer makes the complexity `⊤`. Just before Definition 5.2 they note the alternative of extending a relation to allow every answer on its illegal pairs; their convention for `R` is this one for that extension, which is no harder than `R` -(`Nondeterministic.ecomplexity_le_of_imp`). +(`Nondeterministic.ecomplexity_le_of_imp`). After Definition 5.2 they remark that for relations, +measures such as `N¹(R)` are less interesting, since the answer `1` has no special role. That is +why the relations here have Boolean answers: such a relation is a partial Boolean function, and +`N⁰` and `N¹` keep their meaning. ## Covers and protocols From 8edb0b42db24524956a3463a0b8e2fdc34984250 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:53:02 +0000 Subject: [PATCH 20/23] doc(communication): place the model between total functions and relations It covers partial Boolean functions, the relations with Boolean answers. Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 34 +++++++++---------- 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index 5ba7be44d..279e083b0 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -34,25 +34,23 @@ without rounding. So for such `f`, `ecomplexityFun z f Set.univ Set.univ` is the up to an integer, and for `n ≥ 1` a lower bound `n ≤ ecomplexityFun z f Set.univ Set.univ` says `C^z(f) > 2 ^ (n - 1)`, that is, `N^z(f) > n - 1` in their convention. -The domain sets `A` and `B` and the relations go beyond their Definition 2.1, in the usual way for -partial functions (promise problems). A partial function is a function together with the sets `A` -and `B`: its value outside `A × B` does not matter, and rectangles are not required to lie inside -`A × B`. A relation with Boolean answers is a partial function with an arbitrary domain, accepting -both answers outside it, except that it may accept no answer on some pairs. - -Relations with arbitrary answers are the subject of -[Kushilevitz and Nisan, Chapter 5][KushilevitzNisan1997], and `Protocol.ecomplexity` is stated for -them. Kushilevitz and Nisan require a protocol to be correct only on legal inputs, those with some -acceptable answer, and define the other measures for relations "in a similar manner" +The model here lies between the total Boolean functions of their Definition 2.1 and the relations +with arbitrary answers of [Kushilevitz and Nisan, Chapter 5][KushilevitzNisan1997]: it covers +partial Boolean functions, which are relations with Boolean answers. A partial function is a +function together with the sets `A` and `B`, or, when its domain is not a rectangle, a relation that +accepts both answers outside its domain; its values there do not matter, and rectangles are not +required to lie inside the domain. Kushilevitz and Nisan remark after Definition 5.2 that for +relations, measures such as `N¹(R)` are less interesting, since the answer `1` has no special role; +with Boolean answers, `N⁰` and `N¹` keep their meaning. + +Kushilevitz and Nisan require a protocol for a relation to be correct only on legal inputs, those +with some acceptable answer, and define the other measures for relations "in a similar manner" [Kushilevitz and Nisan, Definition 5.2, p. 71][KushilevitzNisan1997]. Here, as for -`Protocol.ecomplexity`, every pair of `A × B` must get an acceptable answer, so a pair of `A × B` -with no acceptable answer makes the complexity `⊤`. Just before Definition 5.2 they note the -alternative of extending a relation to allow every answer on its illegal pairs; their convention -for `R` is this one for that extension, which is no harder than `R` -(`Nondeterministic.ecomplexity_le_of_imp`). After Definition 5.2 they remark that for relations, -measures such as `N¹(R)` are less interesting, since the answer `1` has no special role. That is -why the relations here have Boolean answers: such a relation is a partial Boolean function, and -`N⁰` and `N¹` keep their meaning. +`Protocol.ecomplexity`, which is stated for relations, every pair of `A × B` must get an acceptable +answer, so a pair of `A × B` with no acceptable answer makes the complexity `⊤`. Just before +Definition 5.2 they note the alternative of extending a relation to allow every answer on its +illegal pairs; their convention for `R` is this one for that extension, which is no harder than +`R` (`Nondeterministic.ecomplexity_le_of_imp`). ## Covers and protocols From 7b1cc6345fe2bb36dd3f98146545b22273a9e30b Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:55:42 +0000 Subject: [PATCH 21/23] =?UTF-8?q?doc(communication):=20relations=20as=20in?= =?UTF-8?q?=20Kushilevitz=E2=80=93Nisan=20Definition=205.1,=20with=20Boole?= =?UTF-8?q?an=20answers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index 279e083b0..406cbf480 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -43,14 +43,18 @@ required to lie inside the domain. Kushilevitz and Nisan remark after Definition relations, measures such as `N¹(R)` are less interesting, since the answer `1` has no special role; with Boolean answers, `N⁰` and `N¹` keep their meaning. -Kushilevitz and Nisan require a protocol for a relation to be correct only on legal inputs, those -with some acceptable answer, and define the other measures for relations "in a similar manner" +A relation `R : X → Y → Bool → Prop` is their relation `R ⊆ X × Y × Z` with `Z = Bool` +[Kushilevitz and Nisan, Definition 5.1, p. 71][KushilevitzNisan1997]: `R x y b` holds exactly when +`(x, y, b) ∈ R`. A partial Boolean function `f` with domain `D` is the relation +`fun x y b => (x, y) ∈ D → f x y = b`. Kushilevitz and Nisan require a protocol for a relation to be +correct only on legal inputs, those with some acceptable answer, and define the other measures for +relations "in a similar manner" [Kushilevitz and Nisan, Definition 5.2, p. 71][KushilevitzNisan1997]. Here, as for `Protocol.ecomplexity`, which is stated for relations, every pair of `A × B` must get an acceptable answer, so a pair of `A × B` with no acceptable answer makes the complexity `⊤`. Just before Definition 5.2 they note the alternative of extending a relation to allow every answer on its -illegal pairs; their convention for `R` is this one for that extension, which is no harder than -`R` (`Nondeterministic.ecomplexity_le_of_imp`). +illegal pairs; their convention for `R` is this one for that extension, which is no harder than `R` +(`Nondeterministic.ecomplexity_le_of_imp`). ## Covers and protocols From 4dec28949a27a7ee63f3948cb5fcf1dec0d0a539 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 04:07:44 +0000 Subject: [PATCH 22/23] =?UTF-8?q?doc(communication):=20cite=20G=C3=B6?= =?UTF-8?q?=C3=B6s=E2=80=93Pitassi=E2=80=93Watson=20Definition=2031=20as?= =?UTF-8?q?=20the=20model=20for=20partial=20functions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds GoosPitassiWatson2018Landscape to references.bib. Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 18 ++++++++++++------ references.bib | 12 ++++++++++++ 2 files changed, 24 insertions(+), 6 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index 406cbf480..441669436 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -36,12 +36,16 @@ up to an integer, and for `n ≥ 1` a lower bound `n ≤ ecomplexityFun z f Set. The model here lies between the total Boolean functions of their Definition 2.1 and the relations with arbitrary answers of [Kushilevitz and Nisan, Chapter 5][KushilevitzNisan1997]: it covers -partial Boolean functions, which are relations with Boolean answers. A partial function is a -function together with the sets `A` and `B`, or, when its domain is not a rectangle, a relation that -accepts both answers outside its domain; its values there do not matter, and rectangles are not -required to lie inside the domain. Kushilevitz and Nisan remark after Definition 5.2 that for -relations, measures such as `N¹(R)` are less interesting, since the answer `1` has no special role; -with Boolean answers, `N⁰` and `N¹` keep their meaning. +partial Boolean functions, which are relations with Boolean answers. For these it is the model NP of +[Göös, Pitassi and Watson, Definition 31][GoosPitassiWatson2018Landscape] (numbered as in ECCC +TR15-049, revision 1): a collection of `2 ^ k` rectangles indexed by `k`-bit witnesses, whose output +is `1` exactly on their union, correct on the domain of the function, of cost `k`; co-classes are +defined by negating the function. A partial function is a function together with the sets `A` and +`B`, or, when its domain is not a rectangle, a relation that accepts both answers outside its +domain; its values there do not matter, and rectangles are not required to lie inside the domain. +Kushilevitz and Nisan remark after Definition 5.2 that for relations, measures such as `N¹(R)` are +less interesting, since the answer `1` has no special role; with Boolean answers, `N⁰` and `N¹` keep +their meaning. A relation `R : X → Y → Bool → Prop` is their relation `R ⊆ X × Y × Z` with `Z = Bool` [Kushilevitz and Nisan, Definition 5.1, p. 71][KushilevitzNisan1997]: `R x y b` holds exactly when @@ -114,6 +118,8 @@ Deterministic protocols give covers directly (`Nondeterministic.ecomplexity_le_p ## References +* [M. Göös, T. Pitassi, T. Watson, *The Landscape of Communication Complexity + Classes*][GoosPitassiWatson2018Landscape], Appendix B * [E. Kushilevitz, N. Nisan, *Communication Complexity*][KushilevitzNisan1997] -/ diff --git a/references.bib b/references.bib index cc6369c43..d521aefdd 100644 --- a/references.bib +++ b/references.bib @@ -2043,6 +2043,18 @@ @article{GoosPitassiWatson2018 doi = {10.1137/16M1059369} } +@article{GoosPitassiWatson2018Landscape, + author = {G{\"o}{\"o}s, Mika and Pitassi, Toniann and Watson, Thomas}, + title = {The Landscape of Communication Complexity Classes}, + journal = {Computational Complexity}, + volume = {27}, + number = {2}, + pages = {245--304}, + year = {2018}, + doi = {10.1007/s00037-018-0166-6}, + note = {Preprint: ECCC TR15-049, revision 1} +} + @article{GotsmanLinial1992, author = {Gotsman, Craig and Linial, Nathan}, title = {The Equivalence of Two Problems on the Cube}, From 360c05283c6ce7d52f9894eef2089ce46528aa5d Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 04:20:40 +0000 Subject: [PATCH 23/23] =?UTF-8?q?doc(communication):=20cite=20G=C3=B6?= =?UTF-8?q?=C3=B6s=E2=80=93Pitassi=E2=80=93Watson=20by=20the=20journal=20n?= =?UTF-8?q?umbering?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../Communication/Nondeterministic/Basic.lean | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean index 441669436..8cf76beae 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -37,15 +37,14 @@ up to an integer, and for `n ≥ 1` a lower bound `n ≤ ecomplexityFun z f Set. The model here lies between the total Boolean functions of their Definition 2.1 and the relations with arbitrary answers of [Kushilevitz and Nisan, Chapter 5][KushilevitzNisan1997]: it covers partial Boolean functions, which are relations with Boolean answers. For these it is the model NP of -[Göös, Pitassi and Watson, Definition 31][GoosPitassiWatson2018Landscape] (numbered as in ECCC -TR15-049, revision 1): a collection of `2 ^ k` rectangles indexed by `k`-bit witnesses, whose output -is `1` exactly on their union, correct on the domain of the function, of cost `k`; co-classes are -defined by negating the function. A partial function is a function together with the sets `A` and -`B`, or, when its domain is not a rectangle, a relation that accepts both answers outside its -domain; its values there do not matter, and rectangles are not required to lie inside the domain. -Kushilevitz and Nisan remark after Definition 5.2 that for relations, measures such as `N¹(R)` are -less interesting, since the answer `1` has no special role; with Boolean answers, `N⁰` and `N¹` keep -their meaning. +[Göös, Pitassi and Watson, Definition B.1, p. 288][GoosPitassiWatson2018Landscape]: a collection of +`2 ^ k` rectangles indexed by `k`-bit witnesses, whose output is `1` exactly on their union, correct +on the domain of the function, of cost `k`; co-classes are defined by negating the function. A +partial function is a function together with the sets `A` and `B`, or, when its domain is not a +rectangle, a relation that accepts both answers outside its domain; its values there do not matter, +and rectangles are not required to lie inside the domain. Kushilevitz and Nisan remark after +Definition 5.2 that for relations, measures such as `N¹(R)` are less interesting, since the answer +`1` has no special role; with Boolean answers, `N⁰` and `N¹` keep their meaning. A relation `R : X → Y → Bool → Prop` is their relation `R ⊆ X × Y × Z` with `Z = Bool` [Kushilevitz and Nisan, Definition 5.1, p. 71][KushilevitzNisan1997]: `R x y b` holds exactly when