Superquadratic sensitivity separation: recursive blocks

This file lifts sensitive blocks of the all-false child input to the next level. A block B of child coordinates is copied into every column of a row i, giving rowLift i B. If the child predicates reject the all-false input but accept it after flipping B, then every next-level predicate accepts the all-false input after flipping rowLift i B. Lifting preserves pairwise disjointness, which yields the block sensitivity lower bound.

Main definitions

• rowLift: the copies of a child block B in all r columns of row i.

Main results

• mem_rowLift: p ∈ rowLift i B iff p lies in row i and p.2 ∈ B.
• rowLift_card: rowLift i B has r * B.card elements.
• rowLift_family_disjoint: pairwise disjoint child blocks lift to pairwise disjoint blocks indexed by Fin k × K.
• recursiveFamily_rowLift: flipping a lifted block in the all-false input makes every next-level predicate accept.

References

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

def Cslib.QueryComplexity.SensitivitySeparation.Internal.rowLift {k r : ℕ} {I : Type} (i : Fin k) (B : Finset I) : Finset ((Fin k × Fin r) × I)

Lift a sensitive block to every column of the specified row.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.mem_rowLift {k r : ℕ} {I : Type} (i : Fin k) (B : Finset I) (p : (Fin k × Fin r) × I) : p ∈ rowLift i B ↔ p.1.1 = i ∧ p.2 ∈ B

A coordinate p lies in rowLift i B iff its row is i and its child coordinate lies in B.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowLift_card {k r : ℕ} {I : Type} (i : Fin k) (B : Finset I) : (rowLift i B).card = r * B.card

The lifted block rowLift i B has r * B.card elements.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowLift_nonempty {k r : ℕ} {I : Type} (i : Fin k) (B : Finset I) (hr : 0 < r) (hB : B.Nonempty) : (rowLift i B).Nonempty

If 0 < r and B is nonempty, then rowLift i B is nonempty.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowLift_family_disjoint {k r : ℕ} {I K : Type} (blocks : K → Finset I) (hB : Pairwise fun (a b : K) => Disjoint (blocks a) (blocks b)) : Pairwise fun (a b : Fin k × K) => Disjoint (rowLift a.1 (blocks a.2)) (rowLift b.1 (blocks b.2))

If the blocks blocks a are pairwise disjoint, then the lifts rowLift a.1 (blocks a.2) indexed by a : Fin k × K are pairwise disjoint.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursiveFamily_rowLift {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hzero : ∀ (q : Fin (h + 1)), (F q fun (x : I) => false) = false) (B : Finset I) (hB : ∀ (q : Fin (h + 1)), F q (flip (fun (x : I) => false) B) = true) (i : Fin k) (q : Fin h) : recursiveFamily T label F q (flip (fun (x : (Fin k × Fin r) × I) => false) (rowLift i B)) = true

If every member of F rejects the all-false input and accepts the all-false input with B flipped, then every next-level predicate accepts the all-false input with rowLift i B flipped.