TITLE
Verifiable Human-AI Exploration of the Lonely Runner Conjecture at k=13:
Cross-Prime Coupling, Exact Evaluation, and Scoped Computational Obstructions

AUTHOR
Lam Nguyen
AI Officer, Real-time Robotics

AI COLLABORATORS (DISCLOSURE, NOT BYLINE AUTHORS)
Sol - ChatGPT 5.6 Thinking
Fable - Claude Code agent

ABSTRACT
The Lonely Runner Conjecture in the integer-speed formulation, denoted LRC(k),
asks whether every k-tuple of distinct positive integer speeds admits a time
at which every runner is at distance at least 1/(k+1) from the origin modulo
one. Recent computer-assisted work establishes LRC(k) for k <= 12, leaving
k = 13, corresponding to fourteen runners, as the first unresolved case.
This paper reports HIVE-LRC, a verifier-linked human-AI research program
conducted through gates D20-D34. It does not claim a proof or a counterexample
for LRC(13). We present four scoped mathematical results: a local orbit-content
reduction; Q13, a sound and non-vacuous cross-prime bounded-square predicate;
a top-residue coset theorem; and an additive symbolic-separability theorem.
We also present a certified exact Q13 evaluator using enumeration,
meet-in-the-middle, and q-scan with an honest OPEN-INCOMPLETE state. Complete
finite-domain experiments show exact pruning and independent implementation
agreement, while target-scale analysis exposes walls in root matching,
residue seeding, and globally coupled symbolic construction. Under frozen
resource caps, no implemented route produced a complete k=13 campaign.
Every negative conclusion is explicitly scoped. The program is archived
without a terminal theorem: a research-allocation decision, not an
impossibility result.

PRIMARY CATEGORY
math.CO

SUGGESTED CROSS-LISTS
math.NT
cs.DM

MSC
11K60; 11A07; 68V15

COMMENTS
Research report; no claim that LRC(13) is solved or refuted.
Includes an AI-use and contribution disclosure.
