Formalizing Structural Graph Theory in Lean 4

Relation to existing catalog entries. Theorem Ramsey formalizes Ramsey’s theorem for graphs (monochromatic clique or independent set). Lemma BipartiteRamsey is a bipartite Ramsey statement in a graph-theoretic form (either a set with no common neighbor, a \(1\)-subdivision of \(K_t\), or a high-degree vertex). Neither matches the shape of Mählmann’s Lemma 4.15, which is a coloring Ramsey statement on \(\ell\)-tuples that concludes order-type-uniformity on two sides independently. We therefore give a separate entry.

\(U\)-notation. Mählmann’s Lemma 4.15 is stated with “\(U\)-notation” (p. 27), which elides the specific growth of the Ramsey bound and only asserts that it is some monotone unbounded function of \(n\). We preserve this in the natural-language statement. A Lean-level formalization will need to pick an explicit function.

Intended use. This entry is used by Lemma SubdividedBicliqueRamsey (Mählmann’s Lemma 13.8), which in turn is used in the target Lemma WeaklySparseMonDepIsNowhereDense (Lemma 13.7). The proof of Lemma 13.7 itself does not invoke Lemma 4.15 directly.

Lean encoding: orderType via compare. Mählmann’s \(\operatorname{otp}(a_1, \ldots, a_\ell)\) is a tuple indexed by pairs \((i, j)\) with \(1 \leq i < j \leq \ell\), valued in \(\{<, =, >\}\). Our orderType uses compare : V → V → Ordering on all pairs \((i, j) \in \texttt{Fin } \ell \times \texttt{Fin } \ell\): \[\texttt{orderType}\ a\ (i, j) := \texttt{compare}\ (a\ i)\ (a\ j).\] This is equivalent to the source’s definition: the \(i = j\) diagonal is always eq, and the \(i > j\) half is redundant with the \(i < j\) half (compare is antisymmetric on LinearOrder). We use the full square rather than the strict lower triangle because it is much more convenient in Lean — no coercion machinery around “\(i < j\) as a Fin pair”.

\(U\)-notation packaging. The universally quantified “\(U_{k, \ell_1, \ell_2}\)” of the source becomes an existentially packaged \((U, \texttt{Monotone } U, \forall N, \exists n, N \leq U n)\): \[\exists U : \mathbb{N} \to \mathbb{N},\ \texttt{Monotone } U\ \land\ (\forall N, \exists n, N \leq U\ n) \land \ldots\] Monotone + the unboundedness clause captures “monotone and unbounded in \(n\)” exactly. Downstream uses that need “\(U n \to \infty\) as \(n \to \infty\)” can combine the two.

Coloring shape: curried. The coloring is (Fin \(\ell_1\) → Fin \(n\)) → (Fin \(\ell_2\) → Fin \(n\)) → Fin \(k\) (curried) rather than (Fin \(\ell_1\) × Fin \(\ell_2\)) → Fin \(n\). Minor difference; the curried form is slightly more Lean-idiomatic for subsequent pattern matching over the two tuples separately.

Positivity of \(k\). The Lean contract adds an explicit hypothesis \(\mathtt{hk : 0 < k}\) not present in Mählmann’s source statement. The source uses \([k]\) informally as a \(1\)-indexed set, silently assuming \(k \geq 1\). Without \(\mathtt{0 < k}\) the Lean statement is false at \((k = 0, \ell_i \geq 1, n = 0)\): the colouring \(c\) has empty domain and so exists vacuously, but the required \(f : (\texttt{Fin } \ell_1 \times \texttt{Fin } \ell_1 \to \texttt{Ordering}) \to \ldots \to \texttt{Fin } 0\) has nonempty domain and empty codomain. The hypothesis makes this degeneracy explicit; downstream uses of bipartiteRamsey discharge it trivially.