# Supplementary note — AI-use disclosure and machine cross-checks

(To be attached to the Hexagon deposit as supplementary material.)

## AI-assistance disclosure (good-faith, per Hexagon deposit terms)
This work was produced with substantial assistance from an LLM
(reasoning model, locally hosted), under the direction of the author.
The author independently:
- read the full statement of Erdős 607 on erdosproblems.com and confirmed
  0 existing proof claims and 0 expositions as of 2026-10-08;
- read the full text of Colbourn–Phelps–Rödl (1984) (6-page PDF, obtained
  via mathdoc.fr) and verified Theorem 2.4 verbatim: "Let g(n) be the
  number of profile sets of n-element PBD's then exp(c1√n) < g(n) <
  exp(c2√n)";
- verified the 3-step reduction is airtight given that theorem.
The proof content of the main note (Steps 1–3) is short and fully
inspected line-by-line by the author.

## Machine cross-checks (CPU, reproducible)
All scripts are public in the repository accompanying this deposit.

1. `verify_reduction.py` — on 16 test families of point sets (k×k grids,
   fully collinear, general position, collinear bundles, random, cross),
   verifies (V1) every pair of points lies in exactly one line-block and
   (V2) the set of block sizes equals A(P). Result: ALL 16 PASS.
2. `verify_lemma.py` — an independent 3-step upper bound that does NOT
   use design theory: Erdős–Davenport–Trotter (1985) |A|≤2√n via
   Gyarfas (2002) Cor. 1; union bound ΣA ≤ 3n; exact knapsack count of
   subsets with sum ≤ 3n → exp(O(√n)). Result: PASS (same order).
3. CPR1984 Theorem 2.4 — quoted verbatim from the primary PDF (see above),
   not from a secondary source.

## Status of formalization
A machine-checked Lean formalization (target: Palomar registry) is in
progress and will be linked from this deposit when accepted.