Odd-restricted Vinogradov estimate at the sharp block count (source Corollary 3.5)

Corollary 3.5 at the sharp block count: a range of odd integers of width $2q$ costs one block, not two.

Let $q\ge1$, let $A\ge0$ and $B\ge0$, let $a'$ be an integer coprime to $q$, and let

Then for all real $\theta$ and all real endpoints $x<y$ with $y-x\le 2q$,

where $\mathrm{vmin}(A,B,\alpha,\theta;z)$ is $A$ when $\sin(\pi\alpha z+\theta)=0$ and $\min\bigl(A,\frac B{|\sin(\pi\alpha z+\theta)|}\bigr)$ otherwise.

This is the source's Corollary 3.5 restricted to the case that actually occurs in Section 5.2, and the restriction matters. As published, Corollary 3.5 carries the covering count $\lfloor\frac{y-x}{2q}\rfloor+1$. On a block $2jq+\frac q2<d\le2(j+1)q+\frac q2$, whose width is exactly $2q$, that count evaluates to $\lfloor1\rfloor+1=2$; but the number of blocks of length $L$ needed to cover a range of width $W$ is $\lceil W/L\rceil$, and $\lfloor W/L\rfloor+1$ exceeds it exactly when $L$ divides $W$. Here $L=2q$ and $W=2q$, so the correct count is $1$.

The source's own proof produces the sharp count. Writing $n=2m+1$ turns the left-hand side into

because $\pi\alpha(2m+1)+\theta=\pi(2\alpha)m+(\pi\alpha+\theta)$. The $m$-range has width $\frac{y-x}2\le q$, so Lemma 3.4 applies to it with one block. The doubling of the admissible width from $q$ to $2q$ and the doubling of the frequency from $\alpha$ to $2\alpha$ are the same phenomenon seen from the two sides of the reindexing; nothing in the argument asks for two blocks.

The constant is decided here. Carrying the published count instead of the sharp one doubles the coefficient of the second term of the source's display (5.17) from $0.89$ to $1.78$, and the platform's Type I right-hand side does not accommodate that: the assembled bound then overshoots by a factor $1.29$ in the worst admissible corner.

Formalization note. The summation range is $(x,y]_{\mathbb Z}$, realized as zIoc, and the summand uses the explicit if convention at the zeros of the sine, since Lean's real division returns $0$ there and a bare min would silently contribute $0$ instead of $A$. The reindexing is stated over $\mathbb Z$ rather than $\mathbb N$ because Int.floor is not clamped at zero, which makes the index-set identity exact and, more importantly, makes the reflection argument (odd_symm_min_sum_le, in the same definition module) expressible at all. The hypothesis $2\alpha=\frac{a'}q+\beta$ is exactly the hypothesis of Corollary 3.5 as stated in the source.