# Canonical pair positions: reproduced evidence and a counterexample

2026-09-05. Exact computational audit; no change to the published SWC paper.

## Outcome

The supplied 75-case experiment reproduces, but the universal canonical
pair-position statement is false. The primitive open speed set

    V = (44, 60, 104, 205),  n=4,  N=5

has no canonical witness under either supplied target list, even when the
requirement gcd(m,q)=1 is removed. This does not refute Lonely Runner.

The set is primitive since gcd(V)=1. It is open in the specified sense:
2 and 4 divide 44; 3 and 5 divide 60. At t=9/148, its distances from integers are

    (12/37, 13/37, 12/37, 69/148).

Their minimum is 12/37 > 1/5. The pair (44,104) has q=148 and mirrored
positions 100/148 and 48/148. Neither orientation is in the original target
list, and distance 48/148 is outside the folded target list.

An independent checker enumerated every m=0,...,q-1 for all six pairs:

| Pair | q | All valid multipliers | Valid original targets | Valid folded targets |
|---|---:|---:|---:|---:|
| (44,60) | 104 | 0 | 0 | 0 |
| (44,104) | 148 | 32 | 0 | 0 |
| (44,205) | 249 | 38 | 0 | 0 |
| (60,104) | 164 | 48 | 0 | 0 |
| (60,205) | 265 | 44 | 0 | 0 |
| (104,205) | 309 | 50 | 0 | 0 |

Thus all 1,239 pair/multiplier seeds are accounted for. There are 212 accepted
seeds in the complete generator and zero in either canonical restriction.
The exact maximum over all time is 12/37 by the established pair-sum
local-maximum theorem (Kravitz, Proposition 2.1). The negative canonical
conclusion itself needs only the finite exhaustive table, not that theorem.

The second primitive example (31,240,450,540,930), n=5, also defeats both
canonical lists without a unit restriction. A separate primitive example
(60,95,110,184) defeats both lists with unit multipliers but can be rescued
by allowing nonunits. Both distinctions are recorded in the evidence.

## Exact statements tested

The original list was implemented literally:

    C(q,N) = {floor(q/N), ceil(q/N), floor(q/N)+1,
              floor(q/2), ceil(q/2)}
             union {floor(kq/d), ceil(kq/d): 2<=d<=6, 1<=k<d}.

The attachment's folded variant uses

    C*(q,N) = {ceil(q/N), ceil(q/N)+1, floor(q/2)}
              union {floor(kq/d), ceil(kq/d): 2<=d<=6, 1<=k<=floor(d/2)},

filtered to ceil(q/N)<=c<=floor(q/2). This is not exactly the same rule:
when q/N is nonintegral it may add ceil(q/N)+1. For example, at q=117,N=8,
the folded list includes 16 while the original list does not. Both rules
were tested separately, with and without gcd(m,q)=1.

All acceptance checks use

    N * min(m*v mod q, q-(m*v mod q)) >= q

for every speed. Equality is retained. This corrects the original prose's
one-sided test c/q>=1/N when c is an oriented residue: that version also
needs c/q<=1-1/N. With a folded distance, just the lower bound is sufficient.

## What reproduced from the supplied files

The two 75-case attachments are identical:

    SHA-256 aeb738d494bb1bdb55b1d35a8928b1f8c42631360d5ff34508eb67c033dd2caf

Every one of their 1,588 listed pair/multiplier rows is a valid witness. All
75 reported maxima, witness validity checks, and least-denominator claims
also agree with exact independent recomputation. All 75 have an expanded
canonical witness with a unit multiplier.

There are 12,742 open seven-element subsets of {1,...,20}. Of these, exactly
12,673 have gcd 1. The reported total therefore assumes primitive speed sets;
this assumption was absent from the proposed universal statement.

Using primitive open sets, rounded floor/ceiling targets, and only coprime
anchor pairs reproduces the original numbers exactly:

| Original proposal | Successful sets | Total |
|---|---:|---:|
| Rounded half-turn | 10,890 | 12,673 |
| Rounded halves, thirds, quarters | 12,598 | 12,673 |
| Expanded original C with all gcd lifts and unit multipliers | 12,673 | 12,673 |

The 75 failures of the second line match the supplied list exactly. This
establishes the source of the reported 85.9% and 99.4% figures. Exact targets
1/2,1/3,1/4 would not work on open sets: some speed is divisible by each small
denominator. These are rounded near-target positions.

Two labeling corrections matter:

* The listed positions are folded distances. Exactly 794 rows disagree with
  the header's oriented-residue definition but agree with the folded one.
* The file contains all unit-multiplier rows. It omits 612 valid non-unit
  pair/multiplier rows, so "every lonely time" needs that qualifier.

Boundary distance 1/8 occurs in 172 rows and 34 of the 75 sets. By set
coverage, 2/15 occurs in more sets (38). None of the 75 sets is actually
tight: every listed exact maximum is strictly larger than 1/8. A frequent
boundary witness should not be conflated with an extremal speed set whose
global maximum equals the threshold.

The 11 inline residual sets are a subset of these 75 and all have expanded
canonical witnesses. The explicit example in the message is valid:
(4,10), q=14, m=11 gives t=11/14 and folded distance 1/7.

The original 5,300 random open tuples were not supplied, so that count has
not been independently reproduced.

## Smaller boxes and search outside them

| n | Maximum speed | All tuples | Open tuples | Primitive open tuples | Primitive failures of either list |
|---:|---:|---:|---:|---:|---:|
| 4 | 24 | 10,626 | 3,266 | 3,019 | 0 |
| 5 | 22 | 26,334 | 7,166 | 6,875 | 0 |
| 6 | 21 | 54,264 | 12,630 | 12,527 | 0 |
| 7 | 20 | 77,520 | 12,742 | 12,673 | 0 |

There are four nonprimitive unit-restricted failures in the first box; the
other displayed boxes have none. The absence of primitive failures in these
boxes does not survive extension to larger speeds, as the counterexamples
above show.

The first primitive unit-only failure was found in a seeded mixture of random
open tuples and divisor-rich tuples (seed 20260906, n=4, sampled speeds up to
200). A second seeded search (20260907, n=4, sampled speeds up to 400) found
(44,60,104,205), which defeats even unrestricted multipliers. Exact checking
of the fixed reported counterexample is independent of the search history.

## Arithmetic lemmas that survive

### Unit solvability

For q=v_i+v_j, g=gcd(v_i,q), the congruence v_i*m=c mod q has a unit solution
modulo q exactly when

    g divides c and gcd(c/g,q/g)=1,

equivalently gcd(c,q)=g. The first requirement gives one reduced root b modulo
Q=q/g. The second says b is a unit modulo Q. For primes dividing q but not Q,
choose a lift that is nonzero modulo each such prime; the Chinese remainder
theorem permits these choices simultaneously. This proves sufficiency.
Necessity follows by taking gcd with q. In fact the number of unit roots is
phi(q)/phi(Q), since reduction of unit groups from q to Q is surjective.
This is elementary modular arithmetic, not a claimed new theorem.

### Small denominator certificate

If some r with 2<=r<=n+1 divides no speed, then t=1/r works: every nonzero
residue has distance at least 1/r>=1/(n+1). It is correct to use this first.

### Scale obstruction to unnormalized canonical lists

For V0=(1,2,3,5,7,8,18), exhaustive pair enumeration gives only the folded
accepted pair distances {2/13,3/23,2/15}. For V=120h*V0, h>=1, all fraction
targets with denominators 2..6 or 8 are integral before rounding. Any target
that is reachable has the corresponding exact fractional position. None
matches those three accepted distances. The extra boundary target plus one
cannot be reached because every speed and pair sum is divisible by 120h.
Thus both proposed canonical lists fail on this entire nonprimitive family,
even though scaling preserves lonely witnesses. Normalization repairs this
particular obstruction; it does not repair the primitive counterexample.

## Concrete improvement to SWC

The new complete search interface normalizes the input and transports the
witness time back by dividing it by the common gcd. It then tries:

    small denominator -> unit canonical proposal -> nonunit canonical proposal
                      -> complete pair-sum grid.

The first three are proposal stages. Only the final complete grid may report
absence for one instance, relying on the pair-sum theorem. If that grid is
too large, the result is `budget_exceeded`, not an assertion of nonexistence.

On (44,60,104,205), the canonical support has accepted mass zero, while the
uniform-distinct-grid-then-uniform-m generator has exact accepted mass

    1700086256 / 10310222235 > 0.

The complete interface returns the verified witness 9/148. A support-preserving
mixture with epsilon weight on the complete generator retains at least
epsilon times that positive mass. This is the precise SWC lesson from the
failed conjecture: highly successful finite target proposals still need
certified complete support. The example adds a falsification regression to
the method; it establishes no universal positivity theorem.

## Files, verification, and next theorem target

`swc_canonical_pair.py` implements both target definitions, correct gcd lifts,
unit filtering, witness validation, normalization, and the complete fallback.
`audit_swc_canonical_residuals.py` parses the attachment as data and records
the reproduced corpus. `verify_swc_canonical_obstruction.py` imports none of
the search code and enumerates every candidate multiplier with Fraction
arithmetic. It checks three stored counterexamples.

```sh
python3 -B audit_swc_canonical_residuals.py
python3 -B verify_swc_canonical_obstruction.py evidence/swc-canonical-obstructions.json
python3 -B -m unittest test_swc_canonical_pair test_swc_lonely_runner test_swc_certificate_kernel
```

The combined suite has 45 test methods, including exhaustive unit-congruence
solvability checks for q<50, the supplied example, both canonical failures,
normalization transport, and the complete fallback. This is exact executable
verification, not a proof-assistant formalization or independent peer review.

The next structural question should allow target sets chosen from certified
residue obstructions, or use the modular-cover approach in
`swc-lonely-runner-moonshot.md`. A fixed small list with the tested formulas
cannot supply the required universal theorem. If the conjecture is explicitly
restricted to n=7, this audit has not refuted or proved that restricted version.

Prior source for pair-sum completeness: Noah Kravitz, *Barely lonely runners
and very lonely runners*, Combinatorial Theory 1 (2021), Proposition 2.1:
https://escholarship.org/content/qt3wx931fh/qt3wx931fh.pdf

Text: CC BY 4.0. Original code: Apache-2.0. The site and current public paper
are unchanged by this experimental audit.
