Superquadratic sensitivity separation: tournament counts

Counts the directed edges inside a vertex set of a tournament: a set I spans exactly I.card.choose 2 internal edges, and this number equals the sum of the internal outdegrees. Consequently a set in which every vertex has internal outdegree at most one has at most three vertices; this bounds the number of gate candidates in the recursive construction.

Main definitions

• Tournament.internalEdges: the directed edges with both endpoints in a given set.

Main results

• Tournament.card_internalEdges: a set I spans I.card.choose 2 internal edges.
• Tournament.sum_outdegree_eq: the internal outdegrees sum to the number of internal edges.
• Tournament.card_le_three_of_outdegree_le_one: internal outdegrees at most one force at most three vertices.

References

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

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.internalEdges {k : ℕ} (T : Tournament k) (I : Finset (Fin k)) : Finset (Fin k × Fin k)

Directed edges whose two endpoints both belong to the given vertex set.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.card_internalEdges {k : ℕ} (T : Tournament k) (I : Finset (Fin k)) : (T.internalEdges I).card = I.card.choose 2

A vertex set I spans exactly I.card.choose 2 internal directed edges.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.sum_outdegree_eq {k : ℕ} (T : Tournament k) (I : Finset (Fin k)) : ∑ i ∈ I, (Finset.filter (T.Adj i) I).card = (T.internalEdges I).card

The sum over i ∈ I of the number of outgoing neighbors of i in I equals the number of internal edges of I.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.card_le_three_of_outdegree_le_one {k : ℕ} (T : Tournament k) (I : Finset (Fin k)) (h : ∀ i ∈ I, (Finset.filter (T.Adj i) I).card ≤ 1) : I.card ≤ 3

If every vertex of I has at most one outgoing neighbor in I, then I has at most 3 vertices.