feat(abstracts): explain communication bounds and BPP containment

ComplexityTests.lean

@@ -2,7 +2,9 @@ import ComplexityTests.AWPPAmplification
 import ComplexityTests.AWPPLowness
 import ComplexityTests.Abstracts.All
 import ComplexityTests.Abstracts.CheckTests
+import ComplexityTests.Abstracts.CommunicationTests
 import ComplexityTests.Abstracts.InputLayouts
+import ComplexityTests.Abstracts.SipserLautemannTests
 import ComplexityTests.AdaptivePPT
 import ComplexityTests.Advice
 import ComplexityTests.AffineController

ComplexityTests/Abstracts/CommunicationTests.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+-- upstream: local-only (formal abstract tests)
+
+import ComplexityAbstracts.CommunicationAbstract
+
+/-! # Concrete clients of the communication abstract
+
+Check that its cost/error conditions admit actual protocols and that its finite disjointness
+bound excludes a small communication budget.
+-/
+
+namespace ComplexityTests.Abstracts.CommunicationTests
+
+open ComplexityAbstracts.CommunicationAbstract
+
+/-- Alice sends her bit, and Bob sends the equality verdict. -/
+def oneBitEquality : Protocol 1 :=
+  .alice (fun x => x 0)
+    (.bob (fun y => !y 0) (.output false) (.output true))
+    (.bob (fun y => y 0) (.output false) (.output true))
+
+example : cost oneBitEquality = 2 := rfl
+
+example : ∀ x y, answer oneBitEquality x y = decide (x = y) := by decide
+
+example : (∃ p : Protocol 1,
+    (∀ x y, answer p x y = decide (x = y)) ∧ cost p ≤ 1) ↔ False := by
+  rw [equality (by decide)]
+  decide
+
+-- On zero positions, disjointness is true and the inner product is false.
+example (x y : Input 0) : disjoint x y = true ∧ innerProduct x y = false := by
+  simp [disjoint, innerProduct, Bool.zero_eq_false]
+
+/-- A point mass on an explicit correct tree meets both public conditions. -/
+example : CostAtMost (PMF.pure oneBitEquality) 2 ∧
+    ErrorAtMost (PMF.pure oneBitEquality) (fun x y => decide (x = y)) 0 := by
+  constructor
+  · intro p hp
+    rw [(PMF.mem_support_pure_iff _ _).mp hp]
+    exact le_rfl
+  · intro x y
+    have h : answer oneBitEquality x y = decide (x = y) := by decide +revert
+    simp [PMF.toOuterMeasure_pure_apply, h]
+
+-- This finite consequence is nontrivial despite the large disjointness constants.
+example (μ : RandomizedProtocol (2 ^ 20)) (hc : CostAtMost μ 15)
+    (he : ErrorAtMost μ disjoint (1 / 3)) : False := by
+  have h := disjointness_lower_bound μ hc he
+  norm_num at h
+
+end ComplexityTests.Abstracts.CommunicationTests

ComplexityTests/Abstracts/SipserLautemannTests.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2026 Bolton Bailey, Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey, Samuel Schlesinger
+-/
+
+-- upstream: local-only (formal abstract tests)
+
+import ComplexityAbstracts.SipserLautemannAbstract
+import ComplexityTests.SipserLautemann
+
+/-! # Concrete clients of the public Sipser–Lautemann abstract
+
+The head-bit language has both yes- and no-instances. A two-bit randomized test has error
+exactly one quarter on each input; its native polynomial-time certificate witnesses the public
+BPP definition, and the public containment supplies both alternating descriptions. A deterministic
+version also checks the boundary convention that zero random bits means one possible seed.
+-/
+
+namespace ComplexityTests.Abstracts.SipserLautemannTests
+
+open ComplexityAbstracts.SipserLautemannAbstract
+open Cslib.Complexity.Tests.SipserLautemann
+  (noisyHeadVerifier noisyHeadVerifier_polyTime noisyHeadVerifier_decides)
+
+/-- The language of strings whose first bit is true; the empty string is rejected. -/
+def HeadLanguage : Set (List Bool) := {x | x.headD false = true}
+
+example : [true] ∈ HeadLanguage := rfl
+example : [] ∉ HeadLanguage := by
+  change ¬ false = true
+  decide
+
+/-- Exactly one of the four fair two-bit seeds flips the answer, for either answer. -/
+example (x : List Bool) :
+    (Finset.univ.filter fun r : Fin 2 → Bool =>
+      noisyHeadVerifier (x, List.ofFn r) ≠ x.headD false).card = 1 := by
+  cases h : x.headD false <;> simp only [noisyHeadVerifier, h] <;> decide
+
+/-- The existing total two-bit test satisfies the public native-machine predicate. -/
+theorem noisyHead_polyTime : PolyTimePredicate noisyHeadVerifier :=
+  CookLevinBridge.computableInPolyTime_iff_tidy.mpr noisyHeadVerifier_polyTime
+
+/-- A genuinely randomized witness for the public BPP definition, on a nonconstant language. -/
+theorem head_mem_BPP : HeadLanguage ∈ BPP := by
+  refine ⟨Polynomial.C 2, noisyHeadVerifier, noisyHead_polyTime, ?_⟩
+  exact noisyHeadVerifier_decides
+
+/-- Both alternating descriptions follow from the abstract's public theorem. -/
+example : HeadLanguage ∈ SigmaTwo ∩ PiTwo := sipserLautemann head_mem_BPP
+
+/-- A deterministic test of the same nonconstant language. -/
+def headVerifier (z : List Bool × List Bool) : Bool := z.1.headD false
+
+private theorem headVerifier_polyTime : PolyTimePredicate headVerifier := by
+  apply CookLevinBridge.computableInPolyTime_iff_tidy.mpr
+  change Turing.MultiTapeTM.ComputableTidilyInPolyTime headVerifier
+    (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)
+    Turing.MultiTapeTM.encBool
+  unfold headVerifier
+  fun_prop
+
+-- There is exactly one random seed of length zero, rather than no seeds.
+example : Fintype.card (Fin 0 → Bool) = 1 := by decide
+
+/-- Zero random bits also give a valid public BPP witness: the unique empty seed is correct. -/
+example : HeadLanguage ∈ BPP := by
+  refine ⟨0, headVerifier, headVerifier_polyTime, ?_⟩
+  intro x
+  cases h : x.headD false <;>
+    simp only [HeadLanguage, Set.mem_ofPred_eq, headVerifier, Polynomial.eval_zero, h] <;> simp
+
+end ComplexityTests.Abstracts.SipserLautemannTests

README.md

@@ -57,6 +57,8 @@ the selection is not an exhaustive API reference.
 * [Formula lower bounds: parity and Andreev](abstracts/ComplexityAbstracts/FormulaBoundsAbstract.lean): Tree-shaped computation pays for repeated work: parity requires quadratic leaf size, and Andreev gives a stronger explicit bound.
 * [One-way functions yield pseudorandom generators and adaptive functions](abstracts/ComplexityAbstracts/CryptographyAbstract.lean): One-wayness yields pseudorandomness, from an extra output bit to functions secure against adaptive oracle queries.
 * [Haken: pigeonhole formulas require long resolution proofs](abstracts/ComplexityAbstracts/ResolutionAbstract.lean): The pigeonhole principle has short CNF statements but requires exponentially many resolution lines.
+* [Communication: disjointness and inner product resist randomness](abstracts/ComplexityAbstracts/CommunicationAbstract.lean): Both problems require linearly many communicated bits even with shared randomness and bounded error.
+* [Sipser–Gács–Lautemann: BPP lies in the second polynomial level](abstracts/ComplexityAbstracts/SipserLautemannAbstract.lean): Bounded-error polynomial time admits both existential–universal and universal–existential polynomial descriptions.
 
 ## Build and use
 

abstracts/ComplexityAbstracts.lean

@@ -1,6 +1,8 @@
 import ComplexityAbstracts.BarringtonAbstract
 import ComplexityAbstracts.BarringtonBridge
 import ComplexityAbstracts.Check
+import ComplexityAbstracts.CommunicationAbstract
+import ComplexityAbstracts.CommunicationBridge
 import ComplexityAbstracts.Computation
 import ComplexityAbstracts.ConstantDepthAbstract
 import ComplexityAbstracts.ConstantDepthBridge
@@ -23,6 +25,8 @@ import ComplexityAbstracts.SavitchAbstract
 import ComplexityAbstracts.SavitchBridge
 import ComplexityAbstracts.ShamirAbstract
 import ComplexityAbstracts.ShamirBridge
+import ComplexityAbstracts.SipserLautemannAbstract
+import ComplexityAbstracts.SipserLautemannBridge
 import ComplexityAbstracts.SubsetSumAbstract
 import ComplexityAbstracts.SubsetSumBridge
 import ComplexityAbstracts.TQBFAbstract

abstracts/ComplexityAbstracts/CommunicationAbstract.lean

@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+-- upstream: local-only (formal abstract library)
+
+import ComplexityAbstracts.CommunicationBridge
+
+/-! # Communication: randomness cannot eliminate the need to exchange information
+
+Alice and Bob each hold an `n`-bit string and exchange bits to compute a joint answer.
+Disjointness and parity of the intersection both require linearly many communicated bits,
+even with shared randomness and error at most one third on every input pair.
+
+Local computation is free. Cost is the worst case over inputs and coins; protocols may be
+chosen separately at each input length. Both players learn the answer, so exact deterministic
+equality costs `n + 1` bits for `n > 0`: Alice sends her input and Bob replies with the answer.
+
+The only allowlisted model is the binary protocol tree described below. Cost and per-input
+error are defined here. Lean checks the bridge proofs; `#check_abstract` audits their statement
+dependencies. The disjointness constants are not optimized.
+
+## References
+
+* [B. Kalyanasundaram, G. Schnitger, *The probabilistic communication complexity of set
+  intersection*][KalyanasundaramSchnitger1992]
+* [A. Razborov, *On the distributional complexity of disjointness*][Razborov1992]
+* [E. Kushilevitz, N. Nisan, *Communication Complexity*, Chapters 1–4][KushilevitzNisan1997]
+-/
+
+namespace ComplexityAbstracts.CommunicationAbstract
+
+/-- A bit string is a function assigning a Boolean to each of `n` positions. -/
+abbrev Input (n : ℕ) := Fin n → Bool
+
+/-- A finite binary tree: `output b` is a leaf announcing `b`; `alice send p₀ p₁` branches
+on the bit `send x` of Alice's input, and `bob` branches on Bob's input. The transcript
+determines the current node, so messages may depend on all earlier messages. -/
+abbrev Protocol (n : ℕ) := Cslib.Communication.Protocol (Input n) (Input n) Bool
+
+/-- Follow the sent bits from the root to a leaf and return its announced answer. -/
+def answer {n : ℕ} (p : Protocol n) (x y : Input n) : Bool := p.run x y
+
+/-- Tree depth: leaves cost zero, and sending one bit costs one plus the larger branch cost. -/
+def cost {n : ℕ} (p : Protocol n) : ℕ := p.depth
+
+/-- Shared randomness selects a deterministic tree independently of the inputs.
+`PMF` is a probability distribution with total mass one. -/
+abbrev RandomizedProtocol (n : ℕ) := PMF (Protocol n)
+
+/-- Every tree with positive probability has depth at most `c`, bounding all its branches. -/
+def CostAtMost {n : ℕ} (μ : RandomizedProtocol n) (c : ℕ) : Prop :=
+  ∀ p ∈ μ.support, cost p ≤ c
+
+/-- On each input pair separately, the probability of a wrong answer is at most `ε`.
+The measure sums the probabilities of trees giving a wrong answer; `toReal` returns a real. -/
+def ErrorAtMost {n : ℕ} (μ : RandomizedProtocol n)
+    (f : Input n → Input n → Bool) (ε : ℝ) : Prop :=
+  ∀ x y, (μ.toOuterMeasure {p | answer p x y ≠ f x y}).toReal ≤ ε
+
+/-- The sets of true positions are disjoint exactly when no position is true in both inputs. -/
+def disjoint {n : ℕ} (x y : Input n) : Bool :=
+  decide (∀ i, (x i && y i) = false)
+
+/-- The inner product modulo two: true when an odd number of positions are true in both
+inputs. The sum below uses Boolean multiplication (AND) and addition (XOR). -/
+def innerProduct {n : ℕ} (x y : Input n) : Bool := ∑ i, x i * y i
+
+/-- **Exact equality.** A deterministic protocol deciding equality within `c` bits exists
+exactly when `n + 1 ≤ c`, for positive input length. At length zero, the constant true
+answer costs no communication. -/
+theorem equality {n c : ℕ} (hn : 0 < n) :
+    (∃ p : Protocol n, (∀ x y, answer p x y = decide (x = y)) ∧ cost p ≤ c) ↔ n + 1 ≤ c :=
+  CommunicationBridge.equality hn
+
+/-- **Kalyanasundaram–Schnitger / Razborov.** Even with shared randomness and error at most
+one third, disjointness needs linear communication: `n ≤ 65536*c + 4096`.
+The proof uses Razborov's corruption method, with a variant of his hard distribution. -/
+theorem disjointness_lower_bound {n c : ℕ} (μ : RandomizedProtocol n)
+    (hc : CostAtMost μ c) (he : ErrorAtMost μ disjoint (1 / 3)) :
+    n ≤ 2 ^ 16 * c + 2 ^ 12 :=
+  CommunicationBridge.disjointness μ hc he
+
+/-- **Inner product.** Even with shared randomness and error at most one third,
+computing parity of the intersection requires `n ≤ 2*c + 3`. The proof bounds the
+discrepancy of the inner-product sign matrix using its orthogonal rows. -/
+theorem innerProduct_lower_bound {n c : ℕ} (μ : RandomizedProtocol n)
+    (hc : CostAtMost μ c) (he : ErrorAtMost μ innerProduct (1 / 3)) :
+    n ≤ 2 * c + 3 :=
+  CommunicationBridge.innerProduct μ hc he
+
+/--
+info: 'ComplexityAbstracts.CommunicationAbstract.disjointness_lower_bound' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms disjointness_lower_bound
+
+/--
+info: 'ComplexityAbstracts.CommunicationAbstract.innerProduct_lower_bound' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms innerProduct_lower_bound
+
+/--
+info: abstract audit passed for `ComplexityAbstracts.CommunicationAbstract`: 12 root
+declarations, 95 dependencies checked
+-/
+#guard_msgs (whitespace := lax) in
+#check_abstract ComplexityAbstracts.CommunicationAbstract allowing [
+  Complexity.Computability.Communication.Protocol
+]
+
+end ComplexityAbstracts.CommunicationAbstract

abstracts/ComplexityAbstracts/CommunicationBridge.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+-- upstream: local-only (formal abstract library)
+
+import ComplexityAbstracts.Check
+import Complexity.Computability.Communication.Disjointness
+import Complexity.Computability.Communication.Discrepancy
+
+/-! # Transfer of communication lower bounds to individual protocols
+
+The abstract uses the elementary deterministic protocol tree, but defines its own worst-case
+cost and per-input error conditions. No communication-complexity infimum occurs in its statements.
+-/
+
+namespace ComplexityAbstracts.CommunicationBridge
+
+open Cslib.Communication
+
+theorem equality {n c : ℕ} (hn : 0 < n) :
+    (∃ p : Protocol (Fin n → Bool) (Fin n → Bool) Bool,
+      (∀ x y, p.run x y = decide (x = y)) ∧ p.depth ≤ c) ↔ n + 1 ≤ c := by
+  have h := Protocol.ecomplexityFun_le_iff
+    (f := fun x y : Fin n → Bool => decide (x = y)) (k := c)
+  rw [show Protocol.ecomplexityFun (fun x y : Fin n → Bool => decide (x = y)) = n + 1 from
+    ecomplexity_equality hn] at h
+  norm_cast at h
+  simpa only [funext_iff] using h.symm
+
+/-- Convert the public cost and error conditions to the library's infimum bound. -/
+theorem complexity_le {n c : ℕ}
+    (μ : PMF (Protocol (Fin n → Bool) (Fin n → Bool) Bool))
+    (f : (Fin n → Bool) → (Fin n → Bool) → Bool)
+    (hc : ∀ p ∈ μ.support, p.depth ≤ c)
+    (he : ∀ x y, (μ.toOuterMeasure {p | p.run x y ≠ f x y}).toReal ≤ (1 : ℝ) / 3) :
+    PublicCoin.ecomplexityFun (1 / 3) f ≤ c := by
+  apply (PublicCoin.ecomplexity_le_depth (μ := μ) ?_).trans
+    (PublicCoin.depth_le_iff.mpr fun p hp => by exact_mod_cast hc p hp)
+  intro x _ y _
+  simpa only [PublicCoin.errorProb, ne_comm] using he x y
+
+theorem disjointness {n c : ℕ}
+    (μ : PMF (Protocol (Fin n → Bool) (Fin n → Bool) Bool))
+    (hc : ∀ p ∈ μ.support, p.depth ≤ c)
+    (he : ∀ x y, (μ.toOuterMeasure
+      {p | p.run x y ≠ decide (∀ i, (x i && y i) = false)}).toReal ≤ (1 : ℝ) / 3) :
+    n ≤ 2 ^ 16 * c + 2 ^ 12 := by
+  have h := PublicCoin.le_mul_ecomplexityFun_disjointness_add n
+  have hf : Cslib.Communication.disjointness =
+      (fun x y : Fin n → Bool => decide (∀ i, (x i && y i) = false)) := by
+    funext x y
+    simp only [Cslib.Communication.disjointness, decide_eq_decide]
+  rw [hf] at h
+  have hcost := complexity_le μ _ hc he
+  have hbound : (n : ℕ∞) ≤ 2 ^ 16 * (c : ℕ∞) + 2 ^ 12 :=
+    h.trans (by gcongr)
+  exact_mod_cast hbound
+
+theorem innerProduct {n c : ℕ}
+    (μ : PMF (Protocol (Fin n → Bool) (Fin n → Bool) Bool))
+    (hc : ∀ p ∈ μ.support, p.depth ≤ c)
+    (he : ∀ x y, (μ.toOuterMeasure {p | p.run x y ≠ x ⬝ᵥ y}).toReal ≤ (1 : ℝ) / 3) :
+    n ≤ 2 * c + 3 := by
+  have h := PublicCoin.le_two_mul_ecomplexityFun_dotProduct_add_three n
+  have hcost := complexity_le μ (fun x y => x ⬝ᵥ y) hc he
+  have hbound : (n : ℕ∞) ≤ 2 * (c : ℕ∞) + 3 := h.trans (by gcongr)
+  exact_mod_cast hbound
+
+end ComplexityAbstracts.CommunicationBridge