Completion density in Korten's improved mirror-set argument #
Apply the entropy lemma and improved light-patterns lemma inside the sampled
union fiber. The exact conditional sampling law yields the 31/32 estimate
for the fraction of first-stage modifications with low completion density.
Source: Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221
(2026), https://eccc.weizmann.ac.il/report/2026/221/, Sections 3--4.
The explicit constants here are q = 32768*k*p and completion deficit 194*k.
theorem
Complexity.BooleanAnalysis.projectionAverage_const_mul_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(a : ℝ)
(f : (ι → Bool) → ℝ)
(s x : ι → Bool)
:
theorem
Complexity.BooleanAnalysis.projectionAverage_fiber_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(f : (ι → Bool) → ℝ)
(s x : ι → Bool)
(R u : { i : ι // s i = true } → Bool)
:
projectionAverage (fun (z : { i : ι // s i = true } → Bool) => f (completePattern s x z)) R u = projectionAverage f (fun (i : ι) => if h : s i = true then R ⟨i, h⟩ else true) (completePattern s x u)
theorem
Complexity.BooleanAnalysis.coordinateDensity_eq_projection_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X : Finset (ι → Bool))
(s x : ι → Bool)
:
coordinateDensity X s x = projectionAverage (fun (y : ι → Bool) => if y ∈ X then 1 else 0) (fun (i : ι) => !s i) x
theorem
Complexity.BooleanAnalysis.projectionAverage_uniformDensity_fiber_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X : Finset (ι → Bool))
(s x : ι → Bool)
(hX : (coordinateFiber X s x).Nonempty)
(R u : { i : ι // s i = true } → Bool)
:
projectionAverage (uniformDensity (coordinateFiber X s x)) R u = 2 ^ uniformDeficit (coordinateFiber X s x) * coordinateDensity X (fun (i : ι) => if h : s i = true then !R ⟨i, h⟩ else false) (completePattern s x u)
theorem
Complexity.BooleanAnalysis.expect_coordinateMarginal_comp_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(f : (ι → Bool) → ℝ)
(s : ι → Bool)
(g : ℝ → ℝ)
:
(Finset.univ.expect fun (x : ι → Bool) => g (projectionAverage f s x)) = Finset.univ.expect fun (z : { i : ι // s i = true } → Bool) => g (coordinateMarginal f s z)
theorem
Complexity.BooleanAnalysis.coordinateFiber_light_patterns_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X : Finset (ι → Bool))
(hX : X.Nonempty)
(s : ι → Bool)
{k r : ℝ}
(hk : 1 ≤ k)
(hdef : uniformDeficit X ≤ k)
(hr : 0 ≤ r)
(hr' : r ≤ 1 / (32768 * k))
:
31 / 32 ≤ X.expect fun (x : ι → Bool) =>
bernoulliAverage r fun (R : { i : ι // s i = true } → Bool) =>
if uniformDeficit (coordinateFiber X s x) ≤ 64 * k ∧ (Finset.univ.expect fun (z : { i : { i : ι // s i = true } // R i = true } → Bool) =>
if coordinateMarginal (uniformDensity (coordinateFiber X s x)) R z ≤ 2 ^ (-128 * k - 2) then 1 else 0) ≤ 2 ^ (-64 * k) then
1
else 0
theorem
Complexity.BooleanAnalysis.fiber_completion_density_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X : Finset (ι → Bool))
(s x : ι → Bool)
(hX : (coordinateFiber X s x).Nonempty)
(R : { i : ι // s i = true } → Bool)
{k : ℝ}
(hk : 1 ≤ k)
(hd : uniformDeficit (coordinateFiber X s x) ≤ 64 * k)
(hl :
(Finset.univ.expect fun (z : { i : { i : ι // s i = true } // R i = true } → Bool) =>
if coordinateMarginal (uniformDensity (coordinateFiber X s x)) R z ≤ 2 ^ (-128 * k - 2) then 1 else 0) ≤ 2 ^ (-64 * k))
:
theorem
Complexity.BooleanAnalysis.coordinateDensity_resample_union_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X : Finset (ι → Bool))
(P Q x y : ι → Bool)
:
coordinateDensity X Q (resample P x y) = coordinateDensity X Q (resample (fun (i : ι) => P i || Q i) x y)
theorem
Complexity.BooleanAnalysis.fiber_completion_density_union_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X : Finset (ι → Bool))
(P Q x : ι → Bool)
(hx : x ∈ X)
{k : ℝ}
(hk : 1 ≤ k)
(hd : uniformDeficit (coordinateFiber X (fun (i : ι) => P i || Q i) x) ≤ 64 * k)
(hl :
(Finset.univ.expect fun (z : { i : { i : ι // (P i || Q i) = true } // (P ↑i && !Q ↑i) = true } → Bool) =>
if coordinateMarginal (uniformDensity (coordinateFiber X (fun (i : ι) => P i || Q i) x))
(fun (i : { i : ι // (P i || Q i) = true }) => P ↑i && !Q ↑i) z ≤ 2 ^ (-128 * k - 2) then
1
else 0) ≤ 2 ^ (-64 * k))
:
theorem
Complexity.BooleanAnalysis.bad_modifications_probability_aux_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X : Finset (ι → Bool))
(hX : X.Nonempty)
{k p q r : ℝ}
(hk : 1 ≤ k)
(hdef : uniformDeficit X ≤ k)
(hp : 0 ≤ p)
(hp' : p ≤ 1)
(hq : 0 ≤ q)
(hq' : q ≤ 1)
(hr : 0 ≤ r)
(hr' : r ≤ 1 / (32768 * k))
(hjoint : (p + q - p * q) * r = p * (1 - q))
: