# Verification and scope report

The general theorem is proved in the manuscript by the identity
A_r = union of [kj,kj+r] over 0<=j<=r for integer balls generated by
1,k,k+1. No reduction-modulo-n collision occurs through radius k when
n>k(k+1). Subtracting ball sizes gives 2k-1 and k+1; translation proves
failure at every vertex. Positive increments bound all closed-walk
lengths and give directed girth greater than k.

The independent-part blow-up argument multiplies the two shell sizes
by m and preserves girth. Its projection is a closed walk, not assumed
to be a simple base cycle. Other copies of the root cannot appear in
shells through k.

The standard-library checker completed 3,546 exact checks in normal mode
and again with Python -O, with identical JSON reports. It uses integer
sets, breadth-first search, and a separate all-pairs shortest-path
implementation on the thirteen-vertex witness. All roots are checked
there and in the tested blow-ups. The general family, larger integer
balls, no-loop/no-digon conditions, degree counts, negative k=2 control,
walk endpoints, and recursive neighborhoods are also tested. No floating
arithmetic is used. Finite regression is not proof of an infinite family;
the written argument supplies that proof.

Source definitions were visually checked in Sullivan's official AIM
PDF, pages 1 and 8. Daamouch's 2025 pages 155-156 and 161 were checked
to distinguish the external-neighborhood recursion. The theorem refutes
the printed universal exact-distance assertion, not its k=2 specialization
and not that other recursive convention. No global minimum-order claim
or absolute priority claim is made.

Acceptance is based on the originating researcher's detailed self-audit.
AI assistance is disclosed in the manuscript. Independent peer review and
formal verification have not occurred. Compilation and visual-build
receipts are preserved separately in the package manifest and build record.