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.
• nearestDistance: the Hamming distance from an input to the nearest center.

Main results

• hammingDist_flip_eq_add_one: flipping a coordinate where x agrees with z increases the distance to z by exactly one.
• near_center_unique: for centers more than 2 * (R + 1) apart, at most one center lies within distance R + 1 of any input.
• ballPredicate_sensitivityAt_zero_le: for such centers, 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.
• ballPredicate_eq_nearestDistance: the ball predicate is a threshold on nearestDistance.

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.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.hammingDist_flip_eq_add_one {I : Type} [Fintype I] (x z : I → Bool) (i : I) (hi : x i = z i) : hammingDist (flip x {i}) z = hammingDist x z + 1

If x i = z i, flipping coordinate i of x increases the Hamming distance to z by exactly one.

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.near_center_unique {I C : Type} [Fintype I] (centers : C → I → Bool) (R : ℕ) (hsep : ∀ (a b : C), a ≠ b → 2 * (R + 1) < hammingDist (centers a) (centers b)) (x : I → Bool) {a b : C} (ha : hammingDist x (centers a) ≤ R + 1) (hb : hammingDist x (centers b) ≤ R + 1) : a = b

If distinct centers are at Hamming distance greater than 2 * (R + 1), then any two centers within distance R + 1 of the same input coincide.

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] (centers : C → I → Bool) {R S : ℕ} (hRS : R < S) (x : I → Bool) (i : I) (hS : ballPredicate centers S x = false) (hR : ballPredicate centers R (flip x {i}) = 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] (centers : C → I → Bool) {R S : ℕ} (hRS : R < S) (x : I → Bool) (i : I) (hR : ballPredicate centers R x = true) (hS : ballPredicate centers S (flip x {i}) = false) : False

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

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

Minimum distance to the finite nonempty family of centers.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.ballPredicate_eq_nearestDistance {I C : Type} [Fintype I] [Fintype C] [Nonempty C] (centers : C → I → Bool) (R : ℕ) (x : I → Bool) : ballPredicate centers R x = decide (nearestDistance centers x ≤ R)

For a nonempty family of centers, the radius-R ball predicate accepts x iff nearestDistance centers x ≤ R.