# SWC and lonely runners: exact support, modular coverage, and the next proof obligation

Research checkpoint: 2026-09-05. Experimental development, not a new published
paper or a claim of solving the general conjecture. Classical and published
results below are attributed; no priority claim is made for the elementary
SWC reformulations or inclusion-exclusion arguments.

Follow-up: the original 75-case dataset has now been supplied and audited.
Its reported counts reproduce after gcd normalization. The expanded universal
canonical-position conjecture has a primitive four-speed counterexample, even
without a unit-multiplier restriction. See [the residual findings](swc-canonical-residual-findings.md).
The missing-data statements below describe the earlier checkpoint.

## What the supplied observation does and does not establish

The supplied message reports 85.9% coverage with near-half-turn targets,
99.4% after thirds and quarters, and 75 residual speed sets. The dataset,
definition of "open sets", runner count, rounding protocol, pair selection,
normalization, and raw outputs were not located in the current repositories
or supplied attachments. These figures are recorded as user-reported, not
reproduced. The new pilot below is deliberately identified as a different
corpus and a fully specified different protocol.

Throughout this note, n means the number of positive speeds relative to one
stationary runner, so there are n+1 total runners. Speeds are positive
integers with a common initial position, and the acceptance threshold is
1/(n+1), including equality. This is an existence statement for the chosen
stationary runner; applying it in each relative frame gives the usual problem.
For arbitrary starting phases, the pair-sum formula requires phase offsets
and cannot simply be reused.

## 1. The pairwise-sum reduction is already a theorem

Let f(t)=min_i ||v_i t|| and Q(V)={v_i+v_j : i<j}. Kravitz's published
Proposition 2.1 [1] gives

    max_t f(t) = max_{q in Q(V)} max_{0 <= m < q} f(m/q).

The paper notes earlier appearances of this reduction. Its original stronger
loneliness-spectrum conjecture is not a safe additional premise: Fan and
Sun give counterexamples and an amended conjecture [2]. The pair-sum
local-maximum theorem is unaffected by that counterexample.

Here is the local argument. If a positive local maximum has value below 1/2,
some active triangular-wave branch must increase and another must decrease.
Otherwise a small move in one direction improves every active constraint,
while inactive constraints retain their slack. Write the active equalities
as v_i t=a+f(t), v_j t=b-f(t). Adding gives t=(a+b)/(v_i+v_j).
If f(t)=1/2, every runner is at a half-integer and any pair sum times t is
an integer. Thus the global maximum belongs to the finite pair grids.

Consequently "for every speed set, some pair and multiplier give loneliness
at least 1/(n+1)" is equivalent to the integer lonely-runner conjecture.
Restricting multipliers to a handful of canonical targets is a stronger
heuristic restriction. Its failure does not refute the pair-sum theorem or
the original conjecture.

## 2. Exact arithmetic for non-coprime pairs

For q=v_i+v_j, put g=gcd(v_i,q)=gcd(v_i,v_j). The equation

    v_i m = a (mod q)

has no solution if g does not divide a. Otherwise all its solutions are

    m = m0 + ell*(q/g),  ell=0,...,g-1,
    m0 = (a/g)*(v_i/g)^(-1) (mod q/g).

Proof: divide the congruence by g, invert the resulting unit, and lift the
unique reduced class. All g lifts matter because other speeds can distinguish
them. For example, (6,10,15) has gcd 1 but no coprime pair. At the pair (6,10),
q=16, target a=8 yields m=4 or 12, and t=1/4 is a valid witness.

The new canonical policy quantizes each fraction 1/2, 1/3, 2/3, 1/4, 3/4 on
the reduced grid of size q/g, tries both floor and ceil, multiplies the target
by g, and enumerates every congruence lift. This makes unreachable targets
explicit and preserves reflection symmetry. The original experiment may have
used a different policy, so its percentages cannot be compared directly.

## 3. SWC needs a measure that sees boundary witnesses

A continuous uniform distribution over time need not assign positive mass to
valid witnesses even when they exist. For V=(1,2), threshold 1/3, the good
times in [0,1) are exactly {1/3,2/3}. Their Lebesgue measure is zero.

Define an atomic generator before searching:

1. Choose a distinct q from Q(V) uniformly.
2. Choose m in {0,...,q-1} uniformly.
3. Output time m/q and check all distances exactly.

If C_q counts its accepted multipliers, its accepted mass is

    delta(V) = (1/|Q(V)|) * sum_q C_q/q.

The pair-sum theorem implies delta(V)>0 iff a lonely time exists. For V=(1,2),
delta=2/3 although the continuous accepted mass is zero. More generally,
whenever a witness exists,

    delta(V) >= 1/(|Q(V)| * max Q(V)).

This lower bound is conditional on nonemptiness. It cannot be used as a
positivity proof before proving that at least one grid count is nonzero.

General SWC compilation principle: if a compact optimization problem has a
proved finite candidate set containing a maximizer, give every candidate
positive atomic weight. Existence at the target threshold then becomes
equivalent to positive accepted mass, even at isolated boundary optima.
For approximate or learned candidate sets, a separate completeness theorem
is necessary. A mixture with weight lambda on a proved complete atomic
generator retains at least lambda times that generator's accepted mass.
This is a useful representation change, not a shortcut around satisfiability.

## 4. Certify overlapping exclusions instead of assuming independence

Fix an anchor pair i,j and q=v_i+v_j. Let k=n+1, A be the multipliers that
satisfy the anchor, and B_r subset A those that fail another runner r.
The two anchor distances coincide, so one anchor condition suffices.

For g=gcd(v_i,q), Q=q/g, the exact anchor count is

    |A| = g * max(0, Q - 2*ceil(Q/k) + 1).

For any other speed v_r, its total bad count over the full grid is

    gcd(v_r,q) * (2*ceil((q/gcd(v_r,q))/k) - 1).

These formulas follow because multiplication maps uniformly, with g lifts,
onto the reduced residue grid. Thus a positive anchor count minus the sum
of the full-grid bad counts is an explicit sufficient criterion.

Stronger instance calculations use restricted intersections. With
S_j=sum_{|J|=j} |intersection_{r in J} B_r|, Bonferroni gives

    C_q >= |A|-S_1,
    C_q >= |A|-S_1+S_2-S_3.

Use the maximum of these bounds and zero. A second-order truncation alone
has the wrong direction for a lower bound on the surviving count. Third
order is not always numerically stronger than first order; retain both.
No independence assumption is used. When neither proves positivity, exact
intersection remains available within the configured work budget.

The current implementation enumerates the residues to compute intersections.
It has not demonstrated a runtime advantage over finding a direct witness.
A substantive algorithmic next step is certified floor-sum or congruence
counting that produces the required intersection counts without full scans.

## 5. A real route from finite certificates to an infinite theorem

The September 1, 2026 version of Sungkawichai and Trakulthongchai [4] reports
computer-assisted proofs through thirteen total runners. Its modular sieve
builds on Rosenfeld and Trakulthongchai and the finite reduction of
Malikiosis, Santos, and Schymura [3]. This is a more concrete moonshot route
than adding induction indices to empirical canonical-target coverage.

For a prime p and lift l, consider EVERY ordered residue tuple modulo lp
whose coordinates are nonzero modulo p. Repeated residues must be included:
distinct integer speeds can coincide modulo lp. A class is proper if it has
a rational witness on the lp grid or an all-but-one gcd reduction specified
in [4, Definition 2.1]. Given LRC(n-1), proving every class proper implies
that p divides the product of speeds in any counterexample to LRC(n).

For primitive minimal counterexamples, the cited reduction gives

    product_i v_i < B_n,
    B_n = (binom(n+1,2)^(n-1)/n)^n.

If independently checked modular covers force divisibility by distinct
primes with product at least B_n, no such counterexample exists. This is a
complete induction step with explicit premises, as in [4, Proposition 2.7].

SWC can represent each direct modular witness by accepted point mass one,
retain each gcd reduction as a dependency on the previous runner theorem,
and combine the finite residue cover with the published product obstruction.
The proof's difficult work is full modular coverage. A large fraction of
covered classes is insufficient.

### Implemented complete small-case reconstruction

The new producer and independent checker certify the following covers for
n=3, hence four total runners:

| Prime p | Lift l | Permutation classes | Ordered tuples |
|---:|---:|---:|---:|
| 2 | 4 | 20 | 64 |
| 3 | 4 | 120 | 512 |
| 5 | 8 | 5,984 | 32,768 |
| 7 | 4 | 2,600 | 13,824 |
| 11 | 4 | 11,480 | 64,000 |

The checker covers 20,204 permutation classes representing 111,168 ordered
tuples, including repeated residues. Each class supplies a checked rational
time or a checked gcd reduction. Prime product 2310 exceeds B_3=1728.

The smaller (3,5,4) grid has 32 uncovered permutation classes, corresponding
to the 192 ordered failures seen in a separate direct sweep. The verifier
rejects it even if its explicit list of failures is forged to be empty.
Lift 8 supplies full coverage. This demonstrates why adaptive lifts are
useful, without asserting every obstruction eventually disappears.

For the remaining induction premise LRC(2), normalize two speeds to coprime
a,b. If both are odd, t=1/2 works. Otherwise q=a+b is odd and the inverse of
a sends (q-1)/2 to a multiplier whose two distances are (q-1)/(2q)>=1/3.
Together with the cited reduction the modular certificates reconstruct the
known four-runner theorem for unbounded integer speeds. The checker reports
the external theorem dependencies explicitly; it does not purport to
formalize these published theorems in a proof assistant.

### Frontier target

Fourteen total runners means n=13. The exact bound is

    B_13 = (91^12/13)^13, approximately 1.34646 * 10^291.

This is a product-of-forced-primes target, not a number of configurations to
test. No n=13 modular cover or prime elimination has been proved here. The
prototype rejects a brute-force frontier cover when it exceeds its work
budget. A scalable attempt needs checked symmetry reductions, compressed
residue-domain covers, adaptive lifting and projection, and independent
verification of every eliminated class.

## 6. Fresh finite pilot

Seed: 20260905. Code uses integers and exact fractions, one process, a
55-second wall limit, and a per-instance work budget. The recorded run
completed in about 20 seconds. It is an independent pilot, not a reproduction
of the user-reported open-set experiment. Random rows are draws without
repeating speeds within a row; rows are not conditioned on being unresolved.

| Corpus | Rows | Half-turn success | Halves/thirds/quarters | Full pair grid |
|---|---:|---:|---:|---:|
| All four-element subsets of 1..14 | 1,001 | 873 | 1,001 | 1,001 |
| Seeded seven-speed draws from 1..160 | 1,000 | 999 | 1,000 | 1,000 |
| Seeded eleven-speed draws from 1..160 | 1,000 | 1,000 | 1,000 | 1,000 |
| Seeded thirteen-speed draws from 1..160 | 300 | 300 | 300 | 300 |

These easy corpora yield no canonical residuals; that is evidence that the
original residual corpus is necessary for a discriminating benchmark.

On the first 40 rows of each corpus, some pair has a positive first-order
bound in 40,12,7,8 rows respectively. Some pair has a positive third-order
bound in all 40 rows of each diagnostic subset. Independent rational interval
intersection agrees with grid existence in all 160 comparisons. These are
retrospective pilot observations, not universal coverage or held-out speedups.

The exact grid verifier uses Fraction arithmetic and imports no producer
functions. The modular verifier reconstructs the complete residue domain
instead of trusting a claimed number of cases. Thirteen new test methods
exercise congruence lifting, isolated witnesses, independent interval checks,
wrong masses, altered maximizers, missing modular classes, invalid gcd
reductions, repeated primes, failed covers, and computation limits. The 24
existing SWC-kernel tests also pass. These tests do not establish the absence
of implementation bugs.

## 7. Concrete research agenda

1. Import the original speed tuples and residual list with hashes. Reproduce
   the precise rounding, coprimality, normalization, and threshold conventions.
2. Assign each failure to an unreachable target, omitted lift, canonical
   restriction, zero-measure boundary, or genuine unsolved cover class.
3. Compare canonical proposals against exact verification cost, not only hit
   rate. Keep the complete atomic fallback in every proposal mixture.
4. Replace residue enumeration in overlap certificates by certified arithmetic
   counting where possible. Keep upper and lower bounds distinct.
5. Encode modular-domain covers as proof objects with explicit partition and
   symmetry lemmas. Lift only unresolved classes and verify projections.
6. Reconstruct larger established cases before attempting n=13. Publish a
   frontier result only when all required covers and the prime-product bound
   are checked, with the LRC(12) dependency stated and audited.

For general n, a universal theorem constructing enough complete modular
covers would still be required. The current work provides an implemented
proof interface and a complete known small-case demonstration, not that
uniform theorem.

## Sources and commands

[1] Noah Kravitz, *Barely lonely runners and very lonely runners: a refined
approach to the Lonely Runner Problem*, Combinatorial Theory 1 (2021), #17,
Proposition 2.1. https://escholarship.org/content/qt3wx931fh/qt3wx931fh.pdf

[2] Ho Tin Fan and Alec Sun, *Amending the Lonely Runner Spectrum Conjecture*.
https://arxiv.org/abs/2306.10417

[3] Romanos Diogenes Malikiosis, Francisco Santos, Matthias Schymura,
*Linearly exponential checking is enough for the lonely runner conjecture and
some of its variants*, Forum of Mathematics, Sigma 13 (2025), e164.
https://doi.org/10.1017/fms.2025.10107

[4] Touch Sungkawichai and Tanupat Trakulthongchai, *Eleven, twelve, and thirteen
lonely runners*, arXiv:2604.23906v2, September 1, 2026. Definition 2.1,
Lemma 2.2, Corollary 2.5, Lemma 2.6, Proposition 2.7, and Section 7.
https://arxiv.org/html/2604.23906v2

From research/:

```sh
python3 -B -m unittest test_swc_lonely_runner test_swc_certificate_kernel
python3 -B run_swc_lonely_pilot.py
python3 -B swc_lonely_modular_cover.py
python3 -B verify_swc_lonely_cover.py evidence/swc-lonely-modular-pilot.json
```

Evidence is in `evidence/swc-lonely-pilot.json` and
`evidence/swc-lonely-modular-pilot.json`. The existing website, manuscript,
and publication record have not been changed by this exploratory branch of
the research. Text: CC BY 4.0. Original new code: Apache-2.0.
