Exact counterexample certificates to the shifted lonely runner conjecture for 18 <= n <= 38

The shifted lonely runner conjecture (Blanco–Criado–Santos, arXiv:2603.24784 v4, Conjecture 1.1(ii)) asserts that for distinct positive integer velocities v1,…,vn and any real shifts s1,…,sn there is a time t with dist(si+vit, Z) ≥ 1/(n+1) for all i. It is known to fail for 5 ≤ n ≤ 17 (Blanco–Criado–Santos) and for every n ≥ 95 (Poliakova, arXiv:2609.23952); Zhang (arXiv:2608.13599) asks about 18 ≤ n ≤ 94. We give explicit exact certificates that it fails for every n with 18 ≤ n ≤ 38: distinct positive integers vi and rational shifts si = ai/D for which the n open arcs of radius 1/(n+1) cover the circle. For n ≤ 28 the velocities are {1,…,n}; for 29 ≤ n ≤ 38 they are sets containing smooth numbers up to 76. The exact value γ(v;s) = maxt mini ||si+vit|| is < 1/(n+1) in every case, with 1/γ − (n+1) in [0.0961, 0.1098], hence En ≥ 0.096 in Poliakova’s notation for n = 18,…,38. What was checked. Each certificate was accepted by two checkers of the producer (different criteria and languages, but the same author), and by an independent auditor’s third checker (exact Fractions; interval subtraction and the exact γ). The exact covering statement (∀ real t, some i has |si+vit−k| < 1/(n+1) for an integer k, together with injectivity and positivity of v) was kernel-checked in Lean 4.34.1 by the auditor for all 34 certificates n = 5,…,38 (axioms within propext, Classical.choice, Quot.sound); we re-ran the pinned compile, the repository’s lean_runner file-mode gate and leanchecker for n = 18 and n = 38. This is Tier A pending a statement lock. What this is NOT. For 39 ≤ n ≤ 94 no certificate was found within a 30 core-hour budget (n = 39,…,60 were attempted, n ≥ 61 never) and the question stays open; we do not claim that the shifted conjecture fails for all n ≥ 5. The results are upper bounds Γ(n) < 1/(n+1) only, with no exact γsh values. Nothing is said about the unshifted lonely runner conjecture. To our knowledge these are the first published certificates for 18 ≤ n ≤ 38 (a scoop check on 2026-10-28 and 2026-10-31; residual risk stated in the paper; not a priority claim). We have not contacted the authors of the cited preprints. Limitations. Independently audited by a different AI agent instance (AUDIT.md, ACCEPT_WITH_CORRECTIONS, eight corrections applied); no human audit and no statement lock (owed). Unverified: the repository gates on the 32 Lean files other than n = 18 and 38 (the auditor ran the pinned compile only), scoop completeness, the per-log CPU figures, the producer’s search code (untrusted, not needed for validity). The Elenchus ledger gate exits with code 1 (0 blocking findings, one LEDGER_UNAUDITED_TIER_A flag per Tier A row).