Ordered Ruzsa-Szemeredi Numbers at Matching Size Two
Xidan Song, Ruifeng Cao
math.CO
Aug 9, 2026 · v2
cs.DM
TL;DR
The r=2 peeling characterisation and selected structural lemmas (induced C4 obstruction, component invariance) are formalised in Lean 4 against pinned Mathlib.
Abstract
Bondy and Szwarcfiter defined $\mathrm{ex}^*(n,F)$ as the largest number of edges in an $n$-vertex graph whose edge set partitions into induced copies of $F$; for $F=2K_2$ the deficiency $\binom{n}{2}-\mathrm{ex}^*(n,2K_2)$ is $Θ(n^{3/2})$. We study the ordered relaxation at fixed matching size, in which each part need only be induced in the union of itself with the parts that follow it; write $\mathrm{ORS}_n(r)$ for the largest number of parts, so that $r\,\mathrm{ORS}_n(r)$ is the ordered analogue of $\mathrm{ex}^*(n,rK_2)$. Our main tool is a characterisation valid for every $r$: an ordered decomposition into induced $r$-matchings is a sequence of steps that start from $K_n$ and repeatedly delete a perfect matching from $2r$ vertices currently spanning a clique. Reading a decomposition backwards turns a condition about the ordering into a reachability question that an exhaustive search can settle. For $r=2$ we determine $\mathrm{ORS}_n(2)$ exactly at orders five through nineteen, where it takes the values $1,3,5,8,11,14,19,23,28,34,40,47,54,62,70$, and we confine $\mathrm{ORS}_{20}(2)$ to $\{78,79\}$. The counting bound $\lfloor n(n-4)/4\rfloor$ is attained at orders five through nine and at eleven, and missed by exactly one part at every other order below twenty, so order eleven is an isolated exception, not a parity effect. Across this range the ordered deficiency equals $\frac32n+O(1)$, and along powers of two a dyadic construction keeps it below $O(n\log n)$; whether it is linear for all $n$ is our main open question. The structural results are formalised in Lean 4, and the searches are certified by fail-closed sweeps and an independent checker.
Problem
The paper studies the ordered Ruzsa–Szemerédi number ORS_n(r): the maximum number of size-r matchings that partition a graph's edges such that each matching is induced in the union of itself with all later parts. The focus is matching size r=2, and specifically the ordered deficiency relative to the complete graph.
Approach
An ordered decomposition is shown to be equivalent to a sequence of K_{2r}-peels from K_n, each deleting a perfect matching on 2r vertices that currently span a clique. This turns the question into reachability of remainder graphs. Structural obstructions (induced C4, connectivity, bridgelessness, contraction correspondence) prune the exhaustive searches over cubic and near-cubic remainders. Lower bounds come from heuristic direct peeling of K_n, and an explicit dyadic construction handles powers of two. The r=2 structural results are formalised in Lean 4 with Mathlib. The searches are certified by fail-closed sweeps and an independent checker.
Results
ORS_n(2) is determined exactly for n=5..19, and ORS_20(2) is confined to {78,79}. The counting bound ⌊n(n-4)/4⌋ is attained at n=5–9 and n=11 and missed by one elsewhere, and the deficiency is (3/2)n+O(1) in this range. Along powers of two, the dyadic construction gives deficiency (n/2)log₂ n.
| n | ⌊n(n-4)/4⌋ | ORS_n(2) |
|---|
| 10 | 15 | 14 |
| 11 | 19 | 19 |
| 16 | 48 | 47 |
| 19 | 71 | 70 |
| 20 | 80 | 78–79 |
Counting bound versus exact ORS_n(2) (selected orders)