Superquadratic sensitivity separation: tower

Iterates the recursive construction n times, starting from a base family indexed by its number of predicates. Each level consumes one predicate index, adds a factor Fin k × Fin r to the coordinates, and lifts the base sensitive blocks along rows. The file computes the sizes of the coordinate and block index types and of the lifted blocks, and shows that nestedness, rejection of the all-false input, and acceptance after flipping a block propagate up the tower.

Main definitions

• TowerCoordinates: coordinate type after n recursive levels.
• TowerBlockIndex: index type of the lifted sensitive blocks after n levels.
• towerFamily: the n-fold iterate of recursiveFamily applied to a base family.
• towerBlocks: the base sensitive blocks lifted through n levels by rowLift.
• baseExtension: extension of a family with D indices to all index counts.

Main results

• tower_coordinates_card: there are (k * r) ^ n * Fintype.card I coordinates at level n.
• towerBlocks_card: lifted blocks have r ^ n times the base block size.
• towerBlocks_pairwise: pairwise disjoint base blocks lift to pairwise disjoint blocks.
• towerFamily_nested: nestedness of the base family propagates up the tower.
• towerFamily_zero: rejection of the all-false input propagates up the tower.
• towerFamily_blocks: every tower predicate accepts the all-false input flipped on any lifted block.

References

• Adapted from OpenAI's formalization [OAI26b] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Combinatorics/Sensitivity/Tower.lean), via the complexitylib port [Sch26e] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.TowerCoordinates (k r : ℕ) (I : Type) : ℕ → Type

Coordinate type after the specified number of recursive construction levels.

@[instance_reducible]

instance Cslib.QueryComplexity.SensitivitySeparation.Internal.towerCoordinatesFintype (k r : ℕ) (I : Type) [Fintype I] (n : ℕ) : Fintype (TowerCoordinates k r I n)

The tower coordinate types are finite whenever the base coordinate type is finite.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.TowerBlockIndex (k : ℕ) (K : Type) : ℕ → Type

Index type for the disjoint sensitive blocks after each recursive level.

@[instance_reducible]

instance Cslib.QueryComplexity.SensitivitySeparation.Internal.towerBlockIndexFintype (k : ℕ) (K : Type) [Fintype K] (n : ℕ) : Fintype (TowerBlockIndex k K n)

The tower block index types are finite whenever the base block index type is finite.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.towerFamily {k r : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (n h : ℕ) : Fin h → (TowerCoordinates k r I n → Bool) → Bool

Iterate the tournament construction, adding a predicate index at each preceding level.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.towerBlocks {k r : ℕ} {I K : Type} (blocks : K → Finset I) (n : ℕ) : TowerBlockIndex k K n → Finset (TowerCoordinates k r I n)

Lift the base sensitive blocks through the recursive row products.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.baseExtension {I : Type} (D : ℕ) (F : Fin D → (I → Bool) → Bool) (h : ℕ) (q : Fin h) (x : I → Bool) : Bool

Extend a prescribed initial family to unused index counts without adding assumptions.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.baseExtension_same {I : Type} (D : ℕ) (F : Fin D → (I → Bool) → Bool) : baseExtension D F D = F

At the prescribed index count D, the extension baseExtension D F is F.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.tower_coordinates_card {k r : ℕ} {I : Type} [Fintype I] (n : ℕ) : Fintype.card (TowerCoordinates k r I n) = (k * r) ^ n * Fintype.card I

After n levels there are (k * r) ^ n * Fintype.card I coordinates.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.tower_block_index_card {k : ℕ} {K : Type} [Fintype K] (n : ℕ) : Fintype.card (TowerBlockIndex k K n) = k ^ n * Fintype.card K

After n levels there are k ^ n * Fintype.card K block indices.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.towerBlocks_card {k r : ℕ} {I K : Type} (blocks : K → Finset I) (L : ℕ) (hL : ∀ (b : K), (blocks b).card = L) (n : ℕ) (b : TowerBlockIndex k K n) : (towerBlocks blocks n b).card = r ^ n * L

If every base block has L elements, then every lifted block at level n has r ^ n * L elements.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.towerBlocks_nonempty {k r : ℕ} {I K : Type} (blocks : K → Finset I) (hr : 0 < r) (hne : ∀ (b : K), (blocks b).Nonempty) (n : ℕ) (b : TowerBlockIndex k K n) : (towerBlocks blocks n b).Nonempty

If 0 < r and every base block is nonempty, then every lifted block is nonempty.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.towerBlocks_pairwise {k r : ℕ} {I K : Type} (blocks : K → Finset I) (hd : Pairwise fun (a b : K) => Disjoint (blocks a) (blocks b)) (n : ℕ) : Pairwise fun (a b : TowerBlockIndex k K n) => Disjoint (towerBlocks blocks n a) (towerBlocks blocks n b)

Pairwise disjoint base blocks lift to pairwise disjoint blocks at every level.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.towerFamily_nested {k r : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (n h : ℕ) (hbase : NestedFamily (base (h + n))) : NestedFamily (towerFamily T label base n h)

If the base family base (h + n) is nested, then the n-level tower family with h indices is nested.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.towerFamily_zero {k r : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (hr : 0 < r) (n h : ℕ) (hbase : ∀ (q : Fin (h + n)), (base (h + n) q fun (x : I) => false) = false) (q : Fin h) : (towerFamily T label base n h q fun (x : TowerCoordinates k r I n) => false) = false

If 0 < r and every predicate of base (h + n) rejects the all-false input, then every predicate of the n-level tower family with h indices rejects the all-false input.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.towerFamily_blocks {k r : ℕ} {I K : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (blocks : K → Finset I) (hr : 0 < r) (n h : ℕ) (hzero : ∀ (q : Fin (h + n)), (base (h + n) q fun (x : I) => false) = false) (hblocks : ∀ (b : K) (q : Fin (h + n)), base (h + n) q (flip (fun (x : I) => false) (blocks b)) = true) (b : TowerBlockIndex k K n) (q : Fin h) : towerFamily T label base n h q (flip (fun (x : TowerCoordinates k r I n) => false) (towerBlocks blocks n b)) = true

If 0 < r and every predicate of base (h + n) rejects the all-false input and accepts it after flipping any base block, then every predicate of the n-level tower family with h indices accepts the all-false input flipped on any block towerBlocks blocks n b.