Superquadratic sensitivity separation: recursive failures

For a fixed input x of the recursive construction, a row clause i fails either because the final predicate rejects a target child in row i or because a gate predicate accepts the labeled child along an outgoing edge of i. This file collects these failures, singles out the rows with exactly one failed condition (target candidates and gate candidates) together with a chosen witness, and shows that there are fewer than 16 target candidates (by the good-labeling property) and at most 3 gate candidates (by an internal edge count).

Main definitions

• targetFailures: columns of a row whose target child is rejected by the final predicate.
• gateFailures: outgoing neighbors whose labeled gate child is accepted.
• targetCandidates: rows with exactly one failed target and no failed gate.
• gateCandidates: rows with no failed target and exactly one failed gate.
• targetWitness: a chosen failed target column of a row.
• gateWitness: a chosen failed gate neighbor of a row.

Main results

• targetFailures_singleton: a target candidate has exactly one failed column, its witness.
• gateFailures_singleton: a gate candidate has exactly one failed neighbor, its witness.
• targetCandidates_card: for a good labeling and a nested family there are fewer than 16 target candidates.
• gateCandidates_neighbor: an edge between two gate candidates points to the witness of its source.
• gateCandidates_card: for a nested family there are at most 3 gate candidates.

References

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

def Cslib.QueryComplexity.SensitivitySeparation.Internal.targetFailures {k r h : ℕ} {I : Type} (F : Fin (h + 1) → (I → Bool) → Bool) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) : Finset (Fin r)

The columns of a row whose target predicates reject.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.gateFailures {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) : Finset (Fin k)

Outgoing neighbors whose gate predicates accept, violating their row conditions.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.targetCandidates {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) : Finset (Fin k)

Rows with exactly one failed target and no failed gate condition.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.gateCandidates {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) : Finset (Fin k)

Rows with no failed target and exactly one failed gate condition.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.targetWitness {k r h : ℕ} {I : Type} (F : Fin (h + 1) → (I → Bool) → Bool) (x : (Fin k × Fin r) × I → Bool) (hr : 0 < r) (i : Fin k) : Fin r

Choose a failed target column, with column zero as fallback.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.gateWitness {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) : Fin k

Choose a failed gate neighbor, with the row itself as fallback.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.targetFailures_empty_iff {k r h : ℕ} {I : Type} (F : Fin (h + 1) → (I → Bool) → Bool) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) : targetFailures F x i = ∅ ↔ ∀ (c : Fin r), F (Fin.last h) (recursiveChild x i c) = true

A row i has no failed target if and only if the final predicate F (Fin.last h) accepts every child recursiveChild x i c of that row.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.gateFailures_empty_iff {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) : gateFailures T label F q x i = ∅ ↔ ∀ (j : Fin k), T.Adj i j → F (gateIndex q) (recursiveChild x j (label i j)) = false

A row i has no failed gate if and only if, for every outgoing neighbor j of i, the gate predicate F (gateIndex q) rejects the child recursiveChild x j (label i j).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.targetFailures_singleton {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (hr : 0 < r) (i : Fin k) (hi : i ∈ targetCandidates T label F q x) : targetFailures F x i = {targetWitness F x hr i}

For a target candidate i, the set of failed target columns is exactly {targetWitness F x hr i}.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.gateFailures_singleton {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) (hi : i ∈ gateCandidates T label F q x) : gateFailures T label F q x i = {gateWitness T label F q x i}

For a gate candidate i, the set of failed gate neighbors is exactly {gateWitness T label F q x i}.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.targetCandidates_card {k r h : ℕ} {I : Type} (T : Tournament k) (A : GoodLabeling T r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (hr : 0 < r) : (targetCandidates T A.label F q x).card < 16

For a good labeling A and a nested family F, there are fewer than 16 target candidates: their witnesses form a target assignment that A.label respects on all internal edges.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.gateCandidates_neighbor {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (i j : Fin k) (hi : i ∈ gateCandidates T label F q x) (hj : j ∈ gateCandidates T label F q x) (hij : T.Adj i j) : j = gateWitness T label F q x i

If F is nested and i → j is an edge between two gate candidates, then j is the gate witness of i.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.gateCandidates_card {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) : (gateCandidates T label F q x).card ≤ 3

If F is nested, there are at most 3 gate candidates, since each has internal outdegree at most one among them.