Uniform entropy deficits and coordinate fibers

Definitions for Lemma 4 and the mirror-set argument in Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

A fiber is a set of patterns on the free coordinates, so its deficit is measured in that smaller cube. Logarithms in deficits are base two.

noncomputable def Complexity.BooleanAnalysis.uniformMass {α : Type u_1} [DecidableEq α] (X : Finset α) (x : α) : ℝ

Uniform probability mass on a nonempty finite set; zero off the set. The empty set gives the zero mass function.

Equations

• Complexity.BooleanAnalysis.uniformMass X x = if x ∈ X then 1 / ↑X.card else 0

noncomputable def Complexity.BooleanAnalysis.uniformDeficit {ι : Type u_1} [Fintype ι] (X : Finset (ι → Bool)) : ℝ

Min-entropy deficit of the uniform distribution on a nonempty Boolean cube subset. The real formula takes value card ι at the empty set because Real.logb 2 0 = 0; entropy interpretations require nonemptiness.

Equations

• Complexity.BooleanAnalysis.uniformDeficit X = ↑(Fintype.card ι) - Real.logb 2 ↑X.card

def Complexity.BooleanAnalysis.completePattern {ι : Type u_1} (s x : ι → Bool) (z : { i : ι // s i = true } → Bool) : ι → Bool

Insert a pattern on selected coordinates, retaining x elsewhere.

Equations

• Complexity.BooleanAnalysis.completePattern s x z i = if h : s i = true then z ⟨i, h⟩ else x i

noncomputable def Complexity.BooleanAnalysis.coordinateFiber {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (s x : ι → Bool) : Finset ({ i : ι // s i = true } → Bool)

The fiber of X over the bits of x outside s, represented on the selected-coordinate cube. This is Korten's X_{x,S} inside its own subcube.

Equations

• Complexity.BooleanAnalysis.coordinateFiber X s x = {z : { i : ι // s i = true } → Bool | Complexity.BooleanAnalysis.completePattern s x z ∈ X}

def Complexity.BooleanAnalysis.resample {ι : Type u_1} (s x y : ι → Bool) : ι → Bool

Replace selected coordinates of x by those of y.

Equations

• Complexity.BooleanAnalysis.resample s x y i = if s i = true then y i else x i

noncomputable def Complexity.BooleanAnalysis.coordinateDensity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (s x : ι → Bool) : ℝ

Fraction of the free-coordinate cube over x that belongs to X.

Equations

• Complexity.BooleanAnalysis.coordinateDensity X s x = ↑(Complexity.BooleanAnalysis.coordinateFiber X s x).card / 2 ^ Fintype.card { i : ι // s i = true }

noncomputable def Complexity.BooleanAnalysis.uniformDensity {ι : Type u_1} [Fintype ι] (X : Finset (ι → Bool)) (x : ι → Bool) : ℝ

Density of uniform mass relative to the uniform Boolean cube. Its uniform cube expectation is one when X is nonempty.

Equations

• Complexity.BooleanAnalysis.uniformDensity X x = 2 ^ Fintype.card ι * Complexity.BooleanAnalysis.uniformMass X x