Ordered-weight certificates for odd cycles in dense coprime graphs: A computer-assisted argument for Erdős Problem 883(i)

For A ⊆ {1,…,n}, let G(A) join distinct integers precisely when they are coprime. We present a computer-assisted proof that |A| > ⌊n/2⌋ + ⌊n/3⌋ − ⌊n/6⌋ forces every odd cycle of length at most ⌊n/3⌋ + 1, for every n (the odd-cycle assertion, part (i), of Erdős Problem 883). The central construction chooses an odd skeleton and fills its gaps with distinct common neighbours. An adjusted totient weight absorbs a finite inclusion–exclusion error into a product bound; ordering the interior skeleton by this weight bounds the number of deficient connector lists via a single cumulative count. Even connectors and arbitrary unused connectors provide complementary certificates. Explicit finite-prefix distribution bounds cover all n ≥ 10^8; smaller parameters are covered by arithmetic certificates and proof-producing (LRAT-checked) SAT computations. The certificate archive is an integral part of the argument. This is an alternative argument; related work by Donald Della Pietra and Yicheng Pan is cited. Part (ii) is due to G. N. Sárközy (1999) and is not claimed. AI systems substantially assisted the mathematical development, programming, checking and writing; see AUTHORSHIP.md. No external peer review, prize acceptance, priority ruling, or complete Lean formalisation is claimed.