Superquadratic sensitivity separation: hamming base

This file provides the Hamming-distance facts behind the initial nested predicates. A one-bit flip changes the Hamming distance to any point by at most one, which controls how the indicator ballPredicate of a union of radius-R Hamming balls can change. For well-separated centers a rejected input has sensitivity at most R + 1, and ball predicates with radii R < S have no common sensitive coordinate at an input on which they take the same value.

Main definitions

• ballPredicate: the indicator of the union of radius-R Hamming balls around given centers.

Main results

• ballPredicate_sensitivityAt_zero_le: for centers more than 2 * (R + 1) apart, the radius-R ball predicate has sensitivity at most R + 1 at every rejected input.
• ballPredicate_no_joint_zero, ballPredicate_no_joint_one: for R < S, no one-bit flip changes both the radius-R and the radius-S predicates from a common value.

References

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

def Cslib.QueryComplexity.SensitivitySeparation.Internal.ballPredicate {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) (R : ℕ) (x : I → Bool) : Bool

The union of equal-radius Hamming balls.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.ballPredicate_eq_true {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) (R : ℕ) (x : I → Bool) : ballPredicate centers R x = true ↔ ∃ (c : C), hammingDist x (centers c) ≤ R

ballPredicate centers R x holds iff x is within Hamming distance R of some center.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.ballPredicate_nested {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) {R S : ℕ} (hRS : R ≤ S) (x : I → Bool) (h : ballPredicate centers R x = true) : ballPredicate centers S x = true

Ball predicates are monotone in the radius: for R ≤ S, acceptance at radius R implies acceptance at radius S.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.ballPredicate_sensitivityAt_zero_le {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) (R : ℕ) (hsep : ∀ (a b : C), a ≠ b → 2 * (R + 1) < hammingDist (centers a) (centers b)) (x : I → Bool) (hx : ballPredicate centers R x = false) : sensitivityAt (ballPredicate centers R) x ≤ R + 1

If distinct centers are at Hamming distance greater than 2 * (R + 1), then the radius-R ball predicate has sensitivity at most R + 1 at every rejected input.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.ballPredicate_no_joint_zero {I C : Type} [Fintype I] [Fintype C] [DecidableEq I] (centers : C → I → Bool) {R S : ℕ} (hRS : R < S) (x : I → Bool) (i : I) (hS : ballPredicate centers S x = false) (hR : ballPredicate centers R (BitString.flipOn {i} x) = true) : False

For R < S, if x is rejected at radius S, then no one-bit flip of x is accepted at radius R.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.ballPredicate_no_joint_one {I C : Type} [Fintype I] [Fintype C] [DecidableEq I] (centers : C → I → Bool) {R S : ℕ} (hRS : R < S) (x : I → Bool) (i : I) (hR : ballPredicate centers R x = true) (hS : ballPredicate centers S (BitString.flipOn {i} x) = false) : False

For R < S, if x is accepted at radius R, then no one-bit flip of x is rejected at radius S.