If a formula $φ(x, y)$ has the independence property on $C$, then for a graph $H$ on $m$ vertices take the elements $a₀, …, a_{m-1}$ and color the set $A$ of them and the set $B$ of the elements $b_{ij}$ for the edges $ij$ of $H$. Two distinct elements of $A$ are adjacent in $H$ if and only if they have a common $φ$-neighbor in $B$. So $C$ transduces all graphs. Conversely, a transduction of all graphs produces the incidence graph between ${0, …, m-1}$ and its subsets, so its edge formula has the independence property.

The argument is carried out for the graph classes of the archive and mathlib formulas, and transferred to the graph classes used here and the translation of formulas.

Suppose φ(x̄; ȳ) has the independence property on $C$. The left tuple is not empty, since otherwise all $aᵢ$ agree. By Shelah's reduction, carried out with Ramsey's theorem on finite shattered sequences, some formula $ψ(x; z̄)$ with a single left variable has the independence property, and so has its dual $ψ*(z̄; x)$. Then $ψ*(z̄; x) ∧ ψ*(z̄'; x)$ codes pairs: for tuples $aᵢ$ and $a_{n+j}$ the elements $b_{{k, n+l}}$ satisfy it exactly when $(i, j) = (k, l)$. Among all formulas coding on $C$, with any number of colors, take one of least total arity. If it has two left variables, then either $x$ extends by elements of a color $A$ to a tuple coding $z$ and no other element of a color $C$, which is a coding formula with a single left variable, or a spurious witness gives a coding formula with parameters and fewer left variables. By symmetry the minimal formula is $θ(x, y, z)$ in single variables. With a color $C₀$ for the codes $c_{i,J}$ with $i ∈ J$, the formula $∃z (C₀(z) ∧ θ(x, y, z))$ has the independence property. So $C$ is not monadically dependent.

The argument is carried out for the graph classes of the archive and mathlib formulas, and transferred to the graph classes used here and the translation of formulas.

The proof in the paper. Color a pair of index pairs $((i, i'), (j, j'))$ by the truth values of φ(āᵢ', c_{i,j}) and $ψ(b̄ⱼ', c_{i,j})$, and take homogeneous sets $I$, $J$ by the bipartite Ramsey lemma. Pair up consecutive elements of $I$ and $J$: with ūᵢ = āᵣ āᵣ' for the $2i$-th and $(2i+1)$-st elements $r < r'$ of $I$, likewise $w̄ⱼ$, and $d_{i,j} = c_{r,s}$, the exclusive or $φ(x̄₁, z) ⊕ φ(x̄₂, z)$ holds of ūᵢ', d_{i,j} exactly when $i' = i$: earlier pairs see two equal truth values by homogeneity, the pair itself sees true then false, and later pairs see false twice. The same holds for the columns. Then the formula $γ = ∃z (U(z) ∧ (φ ⊕ φ) ∧ (ψ ⊕ ψ))$, with $U$ coloring the grid points $d_{i, h(J)}$ for $i ∈ J$, encodes membership $i ∈ J$ for an injection $h$ of the subsets of $[k]$ into the columns. By Baldwin–Shelah this bounds $k$, hence the order of the pattern.

The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.

Concatenate the two tuples to one tuple of length $2ℓ$ and apply the Erdős–Rado theorem for order types of tuples to the induced coloring. This gives a set $H$ of size $2m$ on which the color depends only on the order type of the concatenation. Split $H$ into its $m$ smallest elements $I$ and its $m$ largest elements $J$. Every entry from $I$ lies below every entry from $J$, so for $a ∈ I^ℓ$ and $b ∈ J^ℓ$ the order type of the concatenation is determined by the order types of $a$ and $b$. The function $U(t)$ is the largest $m ≤ t$ such that every $n ≥ t$ admits such sets of size $m$ for every coloring. It is non-decreasing by definition and unbounded by the Ramsey step.

The Ramsey core is adapted from lax-345067 (finite Ramsey theorems for pairs and tuples).

The proof in the paper. Color a pair of index pairs $((i, i'), (j, j'))$ by the truth values of φ(āᵢ', c_{i,j}) and $ψ(b̄ⱼ', c_{i,j})$, and take homogeneous sets $I$, $J$ by the bipartite Ramsey lemma. Pair up consecutive elements of $I$ and $J$: with ūᵢ = āᵣ āᵣ' for the $2i$-th and $(2i+1)$-st elements $r < r'$ of $I$, likewise $w̄ⱼ$, and $d_{i,j} = c_{r,s}$, the exclusive or $φ(x̄₁, z) ⊕ φ(x̄₂, z)$ holds of ūᵢ', d_{i,j} exactly when $i' = i$: earlier pairs see two equal truth values by homogeneity, the pair itself sees true then false, and later pairs see false twice. The same holds for the columns. Then the formula $γ = ∃z (U(z) ∧ (φ ⊕ φ) ∧ (ψ ⊕ ψ))$, with $U$ coloring the grid points $d_{i, h(J)}$ for $i ∈ J$, encodes membership $i ∈ J$ for an injection $h$ of the subsets of $[k]$ into the columns. By Baldwin–Shelah this bounds $k$, hence the order of the pattern.

The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.

An $r$-local formula holds of a tuple in a structure if and only if it holds of the tuple in an induced substructure that contains the ball of radius $r$ around the tuple. The quantifiers of the formula are guarded by balls of radius at most $r$ around the tuple, and these balls are the same in the structure and in the substructure, since a walk of length at most $r$ from the tuple uses only relation tuples whose entries lie in the ball.

The formula is translated into the syntax of the normal form of lax-512892, over a vocabulary with one symbol for each relation symbol and a nullary symbol for falsum. Its normal form has radii at most $7^q − 1$ and at most $q + k$ witnesses in each basic local sentence. Every local formula in it has quantifier depth at most $q · (k + q + 2 + 6 · 7^q + 4α)$, a bound that depends on the arity $α$ of the vocabulary but not on its symbols. Back in mathlib's syntax, each ball-restricted quantifier gets a dist-formula guard of quantifier rank at most $7^q + α$, which gives the rank bound $p = q · (k + q + 2 + 6 · 7^q + 4α) + q + k + 2 · 7^q + 2α$.

Let $q' = p(α, q, k)$ be given by $GaifmanLocality$. A formula of rank at most $q$ uses finitely many relation symbols. Over the sublanguage of these symbols it is equivalent, on finite structures, to a Boolean combination of basic $7^q$-local sentences and $7^q$-local formulas of rank at most $q'$. The sentences have the same truth value for both tuples. A local formula holds of a tuple in the structure if and only if it holds in the induced substructure, by $LocalSubstructure$, since the balls of the sublanguage are contained in those of $L$. In the induced substructures, the two tuples satisfy the same formulas of rank at most $q'$.

Let $h = 7^q$ and $r = h + 1$. Expand the colored graph by a relation for every relation symbol with some positions filled by parameters from $U$, and by a unary relation $P_u$ for every $u ∈ U$. Formulas with parameters become formulas of the expansion without parameters and with the same quantifier rank. For a tuple far from $U$, the ball $B$ of radius $h$ around it in the expansion avoids $U$ and its neighbors, so the new relations are trivial on $B$, and the type of rank $q'$ of the tuple in the expansion of $B$ is determined by its type in the colored graph induced on $B$. By $LocalToGlobal$, that type determines the type of rank $q$ in the expansion, hence the type over $U$ in the colored graph. The types of rank $q'$ of $k$-tuples in colored graphs are bounded by the number of their finite codes, which depends on $q$, $k$ and $c$ only.

The bound follows from $SeparatingTypes$, since for a fixed tuple ū from $U$ the type of ā ū over $U$ is determined by the type of ā over $U$. A formula about ā ū becomes a formula about ā of the same quantifier rank when the variables for ū are replaced by the parameters ū.

The finite form of Matoušek's (p, q)-theorem, through ε-nets and the finite minimax theorem. Its statement has the roles of the sides swapped and needs no exception for the vertices of the sample, so it implies the form used here.

The proof in the paper. Group $A$ by neighborhoods in the ball $B$ and $B$ by neighborhoods in $A$. The parameter set consists of representatives of all groups and of a bounded-VC duality sample for every pair of groups of $A$ and for every group of $B$ against the inner ball. The $S$-flip toggles exactly the pairs of atomic types joined by an edge of $G$ between $A$ and $B$. Then $A$ and $B$ are non-adjacent in the flip, the inner ball is unchanged, and it has no edges to the outside of $B$, so the ball of radius $r + 1$ still avoids $A$. The duality is used in a form without exception for the sample, obtained from the concept at the cost of doubling the sample.

Ding, Oporowski, Oxley and Vertigan, Cor. 2.4, through an explicit Ramsey bound and a staircase argument on homogeneous matrices. The number of atomic types of the left side over the right side is the number of distinct neighborhoods. A half-graph with $i ≤ j$ becomes one with $j ≤ i$ by reversing both tuples.