Superquadratic sensitivity separation: labeling events

For a tournament T on k vertices, an injective v : Fin n → Fin k and target labels m : Fin n → Fin r, the labeling event consists of the edge labelings giving every directed edge v i → v j the label m j. Such an event fixes exactly n.choose 2 coordinates, so it has r ^ (k * k - n.choose 2) elements, and a union bound over all v and m bounds the number of bad labelings. The case n = 16 is used to produce good labelings.

Main definitions

• Tournament.labelingEvent: labelings whose edges among the injected vertices carry the labels of their targets.
• Tournament.badLabelings: union of all labeling events for n vertices and r labels.

Main results

• Tournament.mem_labelingEvent_iff: membership in a labeling event for an injective vertex map.
• Tournament.card_labelingEvent: for injective v the event has exactly r ^ (k * k - n.choose 2) elements.
• Tournament.card_badLabelings_le: (T.badLabelings n r).card ≤ k ^ n * r ^ n * r ^ (k * k - n.choose 2).

References

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

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.labelingEvent {k r n : ℕ} (T : Tournament k) (v : Fin n → Fin k) (m : Fin n → Fin r) : Finset (Fin k × Fin k → Fin r)

Labelings whose edges between injected vertices have the prescribed target labels.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.mem_labelingEvent_iff {k r n : ℕ} (T : Tournament k) {v : Fin n → Fin k} {m : Fin n → Fin r} {A : Fin k × Fin k → Fin r} (hv : Function.Injective v) : A ∈ T.labelingEvent v m ↔ ∀ (i j : Fin n), T.Adj (v i) (v j) → A (v i, v j) = m j

For injective v, A ∈ T.labelingEvent v m iff A (v i, v j) = m j whenever T.Adj (v i) (v j).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.card_labelingEvent {k r n : ℕ} (T : Tournament k) [NeZero n] (v : Fin n → Fin k) (m : Fin n → Fin r) (hv : Function.Injective v) : (T.labelingEvent v m).card = r ^ (k * k - n.choose 2)

For injective v, the labeling event has exactly r ^ (k * k - n.choose 2) elements.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.badLabelings {k : ℕ} (T : Tournament k) (n r : ℕ) : Finset (Fin k × Fin k → Fin r)

Union of labeling events over all vertex maps and target-label assignments.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.labelingEvent_subset_bad {k r n : ℕ} (T : Tournament k) {v : Fin n → Fin k} {m : Fin n → Fin r} : T.labelingEvent v m ⊆ T.badLabelings n r

Every labeling event is contained in T.badLabelings n r.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.card_badLabelings_le {k r n : ℕ} (T : Tournament k) [NeZero n] : (T.badLabelings n r).card ≤ k ^ n * r ^ n * r ^ (k * k - n.choose 2)

Union bound: (T.badLabelings n r).card ≤ k ^ n * r ^ n * r ^ (k * k - n.choose 2).