The bounded-round density adversary #
Induct on the remaining messages and maintain Korten's density rectangle.
The finite parameter specialization uses K_i = 194^i*k and
p_i = (32768*194^d*k)^i*p. Bilateral limits at the root avoid a mirror
step for the first message, giving the exponent d-1 for d rounds.
Source: Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/, Sections 2--4.
theorem
Complexity.KarchmerWigderson.RoundProtocol.not_solves_density_internal
{ι : Type u_1}
{M : Type u_2}
[Fintype ι]
[DecidableEq ι]
[Fintype M]
[DecidableEq M]
{d : ℕ}
(P : RoundProtocol ι M d)
{X Y : Finset (ι → Bool)}
{m : ℝ}
(hM : ↑(Fintype.card M) ≤ 2 ^ m)
(k p : ℕ → ℝ)
(hstep : ∀ i < d, 1 ≤ k i ∧ 194 * k i ≤ k (i + 1) ∧ 2 * k i + 2 + m ≤ k (i + 1) ∧ 32768 * k i * p i ≤ p (i + 1))
(hcap : ∀ i ≤ d, p i ≤ 1 / 4)
(h : DensityRectangle X Y (p 0) (k 0))
:
theorem
Complexity.KarchmerWigderson.RoundProtocol.not_solves_bounded_density_internal
{ι : Type u_1}
{M : Type u_2}
[Fintype ι]
[DecidableEq ι]
[Fintype M]
[DecidableEq M]
{d : ℕ}
(P : RoundProtocol ι M d)
{X Y : Finset (ι → Bool)}
{m k p : ℝ}
(hM : ↑(Fintype.card M) ≤ 2 ^ m)
(hk : 1 ≤ k)
(hmk : m + 1 ≤ k)
(hbudget : (32768 * 194 ^ d * k) ^ d * p ≤ 1 / 4)
(h : DensityRectangle X Y p k)
:
theorem
Complexity.KarchmerWigderson.RoundProtocol.not_solves_bilateral_density_with_deficit_internal
{ι : Type u_1}
{M : Type u_2}
[Fintype ι]
[DecidableEq ι]
[Fintype M]
[DecidableEq M]
{d : ℕ}
(P : RoundProtocol ι M (d + 1))
{X Y : Finset (ι → Bool)}
{m p k : ℝ}
(hM : ↑(Fintype.card M) ≤ 2 ^ m)
(hm : 0 ≤ m)
(hk : 1 ≤ k)
(hp : 0 < p)
(hX : X.Nonempty)
(hY : Y.Nonempty)
(hdX : BooleanAnalysis.uniformDeficit X ≤ k)
(hdY : BooleanAnalysis.uniformDeficit Y ≤ k)
(hleft : ∀ x ∈ X, BooleanAnalysis.IsDensityLimit Y p k x)
(hright : ∀ y ∈ Y, BooleanAnalysis.IsDensityLimit X p k y)
(hbudget : (32768 * 194 ^ d * (m + k)) ^ d * p ≤ 1 / 4)
:
theorem
Complexity.KarchmerWigderson.RoundProtocol.not_solves_bilateral_density_internal
{ι : Type u_1}
{M : Type u_2}
[Fintype ι]
[DecidableEq ι]
[Fintype M]
[DecidableEq M]
{d : ℕ}
(P : RoundProtocol ι M (d + 1))
{X Y : Finset (ι → Bool)}
{m p : ℝ}
(hM : ↑(Fintype.card M) ≤ 2 ^ m)
(hm : 0 ≤ m)
(hp : 0 < p)
(hX : X.Nonempty)
(hY : Y.Nonempty)
(hdX : BooleanAnalysis.uniformDeficit X ≤ 1)
(hdY : BooleanAnalysis.uniformDeficit Y ≤ 1)
(hleft : ∀ x ∈ X, BooleanAnalysis.IsDensityLimit Y p 1 x)
(hright : ∀ y ∈ Y, BooleanAnalysis.IsDensityLimit X p 1 y)
(hbudget : (32768 * 194 ^ d * (m + 1)) ^ d * p ≤ 1 / 4)
: