Superquadratic sensitivity separation: recursive children

This file counts the child positions read by a single row clause: the r target children of its own row together with one labeled gate child for each out-neighbour. These two sets are disjoint because tournaments are loopless, so for a regular tournament on 2 * M ^ 2 + 1 vertices every row clause reads exactly r + M ^ 2 children.

Main definitions

• rowChildren: the child positions (j, c) read by the clause of row i.

Main results

• rowChildren_disjoint: the target positions and the gate positions of a row are disjoint.
• rowChildren_card: the clause of row i reads r + d children, where d is the outdegree of i.
• regular_rowChildren_card: in a regular tournament every row clause reads r + M ^ 2 children.

References

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

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

Child positions used by a row clause, including its targets and outgoing gates.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowChildren_disjoint {k r : ℕ} (T : Tournament k) (label : Fin k → Fin k → Fin r) (i : Fin k) : Disjoint (Finset.image (fun (c : Fin r) => (i, c)) Finset.univ) (Finset.image (fun (j : Fin k) => (j, label i j)) (Finset.filter (T.Adj i) Finset.univ))

The target positions (i, c) of row i are disjoint from its gate positions (j, label i j) for the out-neighbours j of i.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowChildren_card {k r : ℕ} (T : Tournament k) (label : Fin k → Fin k → Fin r) (i : Fin k) : (rowChildren T label i).card = r + (Finset.filter (T.Adj i) Finset.univ).card

The clause of row i reads exactly r + d child positions, where d is the outdegree of i.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.regular_rowChildren_card {M r : ℕ} (T : RegularTournament M) (label : Fin (2 * M ^ 2 + 1) → Fin (2 * M ^ 2 + 1) → Fin r) (i : Fin (2 * M ^ 2 + 1)) : (rowChildren T.toTournament label i).card = r + M ^ 2

In a regular tournament on 2 * M ^ 2 + 1 vertices, every row clause reads exactly r + M ^ 2 child positions.