Superquadratic sensitivity separation: recursive definitions

This file defines one level of the recursive construction. Next-level inputs are indexed by (Fin k × Fin r) × I: a row i : Fin k, a column c : Fin r and a child coordinate. Given a tournament T, an edge labeling label and a family F of h + 1 child predicates whose last member is the target predicate, the clause of row i at index q : Fin h asks that every child of row i satisfies the target predicate and that, for each out-neighbour j of i, the child (j, label i j) is rejected by the gate predicate F (gateIndex q). The next-level predicate at q is the disjunction of these clauses.

Main definitions

• recursiveChild: the child input at row j and column c of a next-level input.
• gateIndex: the order-reversing embedding Fin h → Fin (h + 1) selecting gate predicates.
• rowClause: the clause of row i at index q.
• recursiveFamily: the next-level family, the disjunction of all row clauses.

Main results

• recursiveFamily_eq_true_iff: a next-level predicate accepts iff some row clause holds.
• recursiveFamily_nested: the construction preserves nested families.
• recursiveFamily_zero: if 0 < r and every child predicate rejects the all-false input, so does every next-level predicate.
• recursive_coordinates_card: the next level has k * r * Fintype.card I input coordinates.

References

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

def Cslib.QueryComplexity.SensitivitySeparation.Internal.recursiveChild {k r : ℕ} {I : Type} (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) : I → Bool

Restrict a recursive input to one row and column of child coordinates.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.gateIndex {h : ℕ} (q : Fin h) : Fin (h + 1)

The reversed gate index among all indices except the final target index.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.gateIndex_lt_last {h : ℕ} (q : Fin h) : gateIndex q < Fin.last h

Every gate index lies strictly below the target index Fin.last h.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.gateIndex_antitone {h : ℕ} {q q' : Fin h} (hqq : q ≤ q') : gateIndex q' ≤ gateIndex q

gateIndex is antitone: q ≤ q' implies gateIndex q' ≤ gateIndex q.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.gateIndex_strictAnti {h : ℕ} {q q' : Fin h} (hqq : q < q') : gateIndex q' < gateIndex q

gateIndex is strictly antitone: q < q' implies gateIndex q' < gateIndex q.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.rowClause {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) : Bool

A clause uses every target in its own row and one labeled gate per outgoing edge.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.recursiveFamily {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) : Bool

The next-level predicate is the disjunction of the literal row clauses.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowClause_eq_true_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) : rowClause T label F q x i = true ↔ (∀ (c : Fin r), F (Fin.last h) (recursiveChild x i c) = true) ∧ ∀ (j : Fin k), T.Adj i j → F (gateIndex q) (recursiveChild x j (label i j)) = false

The clause of row i at index q holds iff F (Fin.last h) accepts every child (i, c) and F (gateIndex q) rejects the child (j, label i j) for every out-neighbour j of i.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursiveFamily_eq_true_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) : recursiveFamily T label F q x = true ↔ ∃ (i : Fin k), rowClause T label F q x i = true

The next-level predicate at index q accepts x iff some row clause holds at x.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursiveFamily_eq_false_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) : recursiveFamily T label F q x = false ↔ ∀ (i : Fin k), rowClause T label F q x i = false

The next-level predicate at index q rejects x iff every row clause fails at x.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowClause_nested {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 q' : Fin h} (hqq : q ≤ q') (x : (Fin k × Fin r) × I → Bool) (i : Fin k) (hi : rowClause T label F q' x i = true) : rowClause T label F q x i = true

For a nested family F and q ≤ q', the clause of row i at index q' implies the clause of row i at index q.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursiveFamily_nested {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) : NestedFamily (recursiveFamily T label F)

If F is a nested family, then so is recursiveFamily T label F.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursiveFamily_zero {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hr : 0 < r) (hzero : ∀ (q : Fin (h + 1)), (F q fun (x : I) => false) = false) (q : Fin h) : (recursiveFamily T label F q fun (x : (Fin k × Fin r) × I) => false) = false

If 0 < r and every member of F rejects the all-false input, then every next-level predicate rejects the all-false input.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursive_coordinates_card {k r : ℕ} {I : Type} [Fintype I] : Fintype.card ((Fin k × Fin r) × I) = k * r * Fintype.card I

The coordinate type (Fin k × Fin r) × I has k * r * Fintype.card I elements.