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 the clause of row i reads r + d children, where d is the outdegree of i.

Main definitions

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

Main results

• rowChildren_card: the clause of row i reads r + d children, where d is the outdegree of i.

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_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.