# Verification report

Date: 2026-08-30

## Result

`PASS` - the source compiles, the exact checker passes, and all four PDF
pages pass visual review.

## Mathematical audit

- The GAP covering lemma is valid for improper progressions: hP is covered by
  at most h^q translates of P.
- For s<N, every coefficient in an s-fold sum of B is below N; base-N
  uniqueness and stars-and-bars give exactly binomial(s+r,r).
- Parameter choices are ordered correctly: r>d, then k for the doubling
  ratio, then h for polynomial-growth separation, then N>max(k+1,h).
- The strict inequality |A+B|<K|A| follows from r/(k+1)<K-1.
- k>=2 ensures |A|>|B|.
- Any P+X satisfying the target size bound also satisfies |P|<=|P+X|, so the
  absence of a small P already excludes the full proposed conclusion.
- The final substitution d=ceil(c(K)), C=c(K) handles the single AIM
  constant; c(K)<1 is separately impossible.

## Reproducibility

Run `python3 reproducibility/check_counterexample.py`. The script checks many
finite parameter instances and exact cardinality identities. Such checks
support but do not replace the symbolic proof.

## Build and PDF QA

- Engine: Tectonic 0.17.0 with BibTeX
- Pages: 4, US Letter (612 x 792 pt)
- Undefined references/citations: 0
- Overfull/underfull boxes: 0
- LaTeX errors: 0
- Visual inspection: all 4 pages at 144 dpi; formulas, proof transitions,
  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/