# Verification report

Date: 2026-08-29

## Result

`PASS` - the manuscript compiles, its six rendered pages pass visual review,
and its theorem remains within the accepted canonical claim boundary for
`AIM-COMBINATORICS-0233`.

## Mathematical scope checked

The manuscript states and proves the following qualitative resolution. For
fixed `h >= 2`, fixed `d >= 2`, and a fixed natural-valued degree-`d`
polynomial `f`, every `A` with `f(N) subset hA` satisfies

- exponent `4/(3hd)` in the value variable when `h` is even;
- exponent `4/((3h+1)d)` when `h` is odd.

The proof explicitly checks that these are strictly greater than `1/(hd)`.
It does not claim that either exponent is optimal. It separately identifies
the sharp `h = 1` boundary and the elementary universal upper boundary
`1/d`.

## Proof audit

- The finite two-basis lemma includes loops, handles the small-edge case, and
  obtains the required path lower bound by Cauchy-Schwarz.
- For fixed ordered endpoints, a length-two path injects into a repeated
  nonzero difference, giving the matching upper bound.
- Integer values at `d+1` integers imply rational polynomial coefficients;
  clearing one fixed denominator gives the divisor condition on index gaps.
- Eventual strict convexity makes each fixed gap contribute at most one pair.
- Nonnegative summands of a target at most `X` all lie in `A intersect [0,X]`.
- The even case splits all summands into two equal blocks.
- The odd case first separates the easy large-`A` branch, then freezes one
  coordinate on a fibre of size at least `N/(2M)` before splitting the
  remaining terms.
- Conversion from the index variable `N` to the value variable `X` uses
  `f(N) asymptotic a N^d` with positive leading coefficient.

## Reproducibility

The canonical standard-library checker was rerun with:

```sh
python3 problems/AIM-COMBINATORICS-0233/checks/verify_bounds.py
```

Result: `PASS`. Its fresh output matched the canonical recorded output
byte-for-byte. Recorded-output SHA-256:

`0686bd33c3a272ab58697a7653164b892d87968d3985fc1aa26b53cd7af7c486`

The self-contained submission-side checker in `reproducibility/check.py`
repeats the finite two-basis tests, the even/odd reductions, the polynomial
gap-divisor tests, and exact rational exponent comparisons. These finite tests
support, but do not replace, the symbolic proof.

## Literature and novelty boundary

The manuscript attributes the two-basis graph estimate to Erdos-Newman,
notes the stronger Alon-Bukh-Sudakov order-two result in sufficiently large
degree, and does not claim higher-order grouping as new. Adjacent work on
small-product sets and convex sets is distinguished by hypothesis. The
all-polynomial/all-order synthesis and odd fibre argument are described as
"apparently unrecorded," with no absolute novelty assertion.

## Build and PDF QA

- Engine: Tectonic 0.17.0 with BibTeX
- Build result: success
- Pages: 6
- Page size: US Letter, 612 x 792 pt
- Undefined references or citations: none
- Overfull or underfull boxes reported: none
- Visual inspection: all six pages inspected at 144 dpi
- Visual defects: none observed; title, abstract, formulas, section breaks,
  bibliography, margins, and page numbers are legible and unclipped

## Public release and license

The author approved public release on 2026-09-02. This paper, its source files, and this verification report are licensed under the Creative Commons Attribution 4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/