From 90ce2e25eeb263fd67aac9f299cfddf01ebafc24 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 01:01:48 +0000 Subject: [PATCH 01/14] 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 bfb161a8135cf6d1e0f59e96528c6673b8af1461 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:04:05 +0000 Subject: [PATCH 02/14] =?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 d2f69357d3cb2440badd93741e50dbc7915e6713 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:21:37 +0000 Subject: [PATCH 03/14] 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 9b5d8065ccbdccac61f61b6c6f7520cacad6f867 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:56:30 +0000 Subject: [PATCH 04/14] 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 d43f9e9a4ee636d4d811157b03a111f61dbfbac8 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 03:29:03 +0000 Subject: [PATCH 05/14] =?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 06/14] =?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 07/14] 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 08/14] =?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 09/14] 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 10/14] 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 11/14] =?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 12/14] =?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 13/14] =?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 From 18fc9cf2d18f477dc74cf215218be73277b2bb7d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 01:08:49 -0400 Subject: [PATCH 14/14] doc(communication): cite verified author-copy pagination Point Definition B.1 to the NSF-hosted journal-author copy, printed page 44. The journal folio was not directly verified; the mathematical paraphrase, code, clients and bibliography are unchanged. Coordinator documentation fix for PR #1913; preserve the original contribution and independent mathematical review. --- .../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 8cf76beae..f259d0653 100644 --- a/Complexity/Computability/Communication/Nondeterministic/Basic.lean +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -37,7 +37,8 @@ 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 B.1, p. 288][GoosPitassiWatson2018Landscape]: a collection of +[Göös, Pitassi and Watson, Definition B.1][GoosPitassiWatson2018Landscape] +([author copy](https://par.nsf.gov/servlets/purl/10090758), p. 44): 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