Superquadratic sensitivity separation: construction

Assembly of the separating function. The nested Hamming-ball family initialFamily is extended to all index counts, pushed through d recursive tournament levels to obtain terminalPredicate, and M disjoint copies are combined by an OR and reindexed onto Fin (constructionDimension d M r). Under the budget max r 16 / M * 3 ^ (d + 1) ≤ 2, the result has sensitivity at most 2 * (d + 2) * M ^ (d + 1) and block sensitivity at least M ^ 2 * (2 * M ^ 2 + 1) ^ d at the all-false input.

Main definitions

• constructionBase: the initial family, extended to all index counts.
• ConstructionCoordinates: the coordinate type after a given number of recursive levels.
• terminalPredicate: the single predicate remaining after d recursive levels.
• finalBoolean: the OR of M disjoint copies of terminalPredicate.
• constructionDimension: the number (d + 2) * M ^ 2 * ((2 * M ^ 2 + 1) * r) ^ d of coordinates of the final function.
• finalWitness: finalBoolean reindexed onto Fin (constructionDimension d M r).

Main results

• construction_profiles: under the budget, the zero- and one-side sensitivities at level n ≤ d are at most 2 * (d + 2) * M ^ n and 2 * (d + 2) * M ^ (n + 1).
• terminalPredicate_blockSensitivity: the terminal predicate has block sensitivity at least M * (2 * M ^ 2 + 1) ^ d at the all-false input.
• finalWitness_sensitivity: under the budget, sensitivity (finalWitness d T A) ≤ 2 * (d + 2) * M ^ (d + 1).
• finalWitness_blockSensitivity: the final witness has block sensitivity at least M ^ 2 * (2 * M ^ 2 + 1) ^ d at the all-false input.
• final_coordinates_card: the final function has exactly constructionDimension d M r coordinates.

References

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

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

Extend the initial Hamming-ball predicates to all index counts.

@[reducible, inline]

abbrev Cslib.QueryComplexity.SensitivitySeparation.Internal.ConstructionCoordinates (d M r n : ℕ) : Type

Coordinates for the regular-tournament construction at a given level.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.terminalPredicate {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) : (ConstructionCoordinates d M r d → Bool) → Bool

The single remaining predicate after all recursive levels.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.terminalPredicate_blockSensitivity {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) : M * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt (terminalPredicate d T A) fun (x : ConstructionCoordinates d M r d) => false

For 0 < r, the terminal predicate has block sensitivity at least M * (2 * M ^ 2 + 1) ^ d at the all-false input.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.construction_profiles {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hM : 0 < M) (hr : 0 < r) (hbudget : ↑(max r 16) / ↑M * 3 ^ (d + 1) ≤ 2) (n : ℕ) : n ≤ d → towerSide T.toTournament A.label (constructionBase d M) (d + 1) n false ≤ 2 * (d + 2) * M ^ n ∧ towerSide T.toTournament A.label (constructionBase d M) (d + 1) n true ≤ 2 * (d + 2) * M ^ (n + 1)

Under the budget max r 16 / M * 3 ^ (d + 1) ≤ 2, for every level n ≤ d the tower side sensitivity is at most 2 * (d + 2) * M ^ n on rejected inputs and at most 2 * (d + 2) * M ^ (n + 1) on accepted inputs.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.finalBoolean {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) : (Fin M × ConstructionCoordinates d M r d → Bool) → Bool

Disjoin M independent copies of the terminal predicate.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.constructionDimension (d M r : ℕ) : ℕ

Number of coordinates of the final Boolean function.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.final_coordinates_card (d M r : ℕ) : Fintype.card (Fin M × ConstructionCoordinates d M r d) = constructionDimension d M r

The coordinate type of finalBoolean has exactly constructionDimension d M r elements.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.finalWitness {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) : (Fin (constructionDimension d M r) → Bool) → Bool

Reindex the final Boolean function onto an ordinary finite Boolean cube.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.finalWitness_zero {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) : (finalWitness d T A fun (x : Fin (constructionDimension d M r)) => false) = false

For 0 < r, the final witness rejects the all-false input.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.finalWitness_sensitivity {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hM : 0 < M) (hr : 0 < r) (hbudget : ↑(max r 16) / ↑M * 3 ^ (d + 1) ≤ 2) : sensitivity (finalWitness d T A) ≤ 2 * (d + 2) * M ^ (d + 1)

Under the budget max r 16 / M * 3 ^ (d + 1) ≤ 2, sensitivity (finalWitness d T A) ≤ 2 * (d + 2) * M ^ (d + 1).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.finalWitness_blockSensitivity {M r : ℕ} (d : ℕ) (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (hr : 0 < r) : M ^ 2 * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt (finalWitness d T A) fun (x : Fin (constructionDimension d M r)) => false

For 0 < r, the final witness has block sensitivity at least M ^ 2 * (2 * M ^ 2 + 1) ^ d at the all-false input.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.constructionDimension_pos {d M r : ℕ} (hM : 0 < M) (hr : 0 < r) : 0 < constructionDimension d M r

For 0 < M and 0 < r, the construction dimension is positive.