Superquadratic sensitivity separation: initial predicates

This file constructs the base case of the recursive construction: the family initialFamily d M of d + 1 nested predicates on Fin M × Fin (d + 2), where predicate q accepts the inputs within Hamming distance d - q of some row center blockCenter j. The M rows baseBlock j are disjoint sensitive blocks of every predicate at the all-false input, while the sensitivity on rejected inputs is at most d + 2 and the joint sensitivity is zero.

Main definitions

• blockCenter: the indicator of row j of Fin M × Fin L.
• baseBlock: the set of coordinates in row j of Fin M × Fin L.
• initialFamily: the nested family of unions of Hamming balls around the row centers.

Main results

• initialFamily_nested: initialFamily d M is a nested family.
• initialFamily_zero: every predicate rejects the all-false input.
• initialFamily_baseBlock: every predicate accepts the all-false input with a row flipped.
• initialFamily_side_zero: on rejected inputs the sensitivity is at most d + 2.
• initialFamily_side_one: on accepted inputs the sensitivity is at most (d + 2) * M.
• initialFamily_joint: the joint sensitivity of the family is zero.

References

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

def Cslib.QueryComplexity.SensitivitySeparation.Internal.blockCenter {M L : ℕ} (j : Fin M) : Fin M × Fin L → Bool

The Boolean input supported on one row of the base coordinate product.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.baseBlock {M L : ℕ} (j : Fin M) : Finset (Fin M × Fin L)

The coordinates in one row of the base coordinate product.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.mem_baseBlock {M L : ℕ} (j : Fin M) (p : Fin M × Fin L) : p ∈ baseBlock j ↔ p.1 = j

A coordinate lies in baseBlock j iff its row index is j.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.baseBlock_nonempty {M L : ℕ} (hL : 0 < L) (j : Fin M) : (baseBlock j).Nonempty

For 0 < L, each row baseBlock j is nonempty.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.baseBlock_disjoint {M L : ℕ} : Pairwise fun (i j : Fin M) => Disjoint (baseBlock i) (baseBlock j)

Distinct rows baseBlock i and baseBlock j are disjoint.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.initialFamily (d M : ℕ) : Fin (d + 1) → (Fin M × Fin (d + 2) → Bool) → Bool

Nested unions of Hamming balls around the disjoint row centers.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.initialFamily_nested (d M : ℕ) : NestedFamily (initialFamily d M)

initialFamily d M is a nested family: the radius d - q decreases with q, so acceptance at index q' implies acceptance at every index q ≤ q'.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.initialFamily_zero (d M : ℕ) (q : Fin (d + 1)) : (initialFamily d M q fun (x : Fin M × Fin (d + 2)) => false) = false

Every predicate of initialFamily d M rejects the all-false input.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.initialFamily_baseBlock (d M : ℕ) (q : Fin (d + 1)) (j : Fin M) : initialFamily d M q (flip (fun (x : Fin M × Fin (d + 2)) => false) (baseBlock j)) = true

Every predicate of initialFamily d M accepts the all-false input with row j flipped.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.initialFamily_side_zero (d M : ℕ) : sideSensitivity (initialFamily d M) false ≤ d + 2

On rejected inputs, every predicate of initialFamily d M has sensitivity at most d + 2.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.initialFamily_side_one (d M : ℕ) : sideSensitivity (initialFamily d M) true ≤ (d + 2) * M

On accepted inputs, every predicate of initialFamily d M has sensitivity at most (d + 2) * M, the number of coordinates.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.initialFamily_joint (d M : ℕ) (b : Bool) : jointSensitivity (initialFamily d M) b = 0

For either output bit b, the joint sensitivity of initialFamily d M is zero: at an input where predicates q < q' both output b, no coordinate is sensitive for both.