← All papers
First page of An Overlap Construction for Relative Linear Extension Ratios

An Overlap Construction for Relative Linear Extension Ratios

Maseeh Ghodsi

math.CO Jul 11, 2026 · v1
The deductive core—continuant floor bound, residue-counting steps, and case analysis of the main theorem—is machine-checked in Lean 4 using its standard library.
Chan and Pak introduced the relative linear extension ratio $ρ(P,x)=e(P)/e(P-x)$, where $e(P)$ is the number of linear extensions of a finite poset $P$, and let $ν(c,d)$ be the least number of elements of a poset that realizes $ρ(P,x)=d/c$. They proved that $ν(c,d)\le d/c+O(\log d\log\log d)$ for $d\ge 3c$, and asked whether the hypothesis $d\ge 3c$ can be relaxed to $d\ge(1+\varepsilon)c$ or removed. We prove the fixed-gap form of this question: for every fixed $\varepsilon>0$, $ν(c,d)\le \frac{d}{c}+O_{\varepsilon}(\log d\log\log d)$ whenever $d\ge(1+\varepsilon)c$, and the implied constant is absolute once $d\ge 2c$. The new ingredient is a one-element overlap construction: if $x$ is minimal in $P$ and $y$ is minimal in $Q$, then there is a poset $R$ with $|R|=|P|+|Q|-1$ and an element $z$ such that $ρ(R,z)=ρ(P,x)+ρ(Q,y)-1$. Together with the continued-fraction construction of Chan and Pak and Rukavishnikova's tail bound for sums of partial quotients, this removes the factor $3$ in their range. We also show that the fixed-gap hypothesis is essentially optimal for this construction. In the range $1 < d/c < 2$, with $h=d-c$, the size bound the construction can certify is at least $\lfloor c/h\rfloor$, so the method reaches the stated error term only when $h$ is at least of order $c/(\log c\log\log c)$. The remaining obstruction to removing the hypothesis is a short-interval problem for sums of partial quotients, which we describe. The deductive part of the argument has been checked with the Lean proof assistant.

Chan and Pak defined the relative linear extension ratio ρ(P,x)=e(P)/e(P-x) and ν(c,d), the least size of a poset realizing ρ=d/c, proving ν(c,d)≤d/c+O(log d log log d) for d≥3c. They asked whether the hypothesis d≥3c can be relaxed to d≥(1+ε)c or removed.

A one-element overlap construction is introduced: for minimal x∈P and y∈Q, a poset R with |R|=|P|+|Q|-1 satisfies ρ(R,z)=ρ(P,x)+ρ(Q,y)-1, merging the two auxiliary elements of the earlier flip-flop construction. Combined with the continued-fraction construction and Rukavishnikova's tail bound for sums of partial quotients, this removes the factor 3. The deductive part is checked in Lean 4: the continuant floor bound, the two residue-counting injections and pigeonhole choice are proved unconditionally, and the main theorem is formalized conditionally on three imported inputs, with the overlap identity verified by exhaustive enumeration.

For every fixed ε>0, ν(c,d)≤d/c+O_ε(log d log log d) whenever d≥(1+ε)c, with an absolute implied constant once d≥2c. The fixed-gap hypothesis is shown essentially optimal for this construction, since for 1<d/c<2 with h=d-c the certifiable size is at least ⌊c/h⌋.