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 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_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_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 (BitString.flipOn (blocks b) fun (x : I) => false) = true) (b : TowerBlockIndex k K n) (q : Fin h) : towerFamily T label base n h q (BitString.flipOn (towerBlocks blocks n b) fun (x : TowerCoordinates k r I n) => false) = 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.