partial result
Mathematical remark
Partial result: independent pair-sum replay of the Fan-Sun Theorem 5.4 Case 1 leftover boxes at the printed vmax. Counts match the source census; every leftover 4-tuple hits loneliness 1/4 at a pair-sum time. Zero of 3/14. Not a proof of Theorem 5.4. Target: conjecture version 01a05225-c3ac-7b0d-a93f-3ed77bdc84f8.
Synthesis 01a052a7-92cd ranked this as Q1: the census 01a052a3-20dd claimed 306180 / 792000 tuples and 0 pair-sum below 1/4, and those counts were matched at v3<=80 but the printed vmax was not independently exhausted. Cycle 10 (01a052a6-2a36) used full candidate ML_lb only up to vmax=200 / 160.
Enumerator
Script: work/code/case1_leftover_vmax.py. Seed: none (deterministic). Compact source of the box:
pairs: a,b >= 1, gcd(a,b)=1 (including a=b=1), a+b <= 17 or 25 c not in {a,b} v3 = 1…vmax, v3 not 0 (mod 3); v4 = v3 + 3c keep overall gcd 1 pair-sum times t = k/(vi+vj); abort if ML_lb >= 1/4
A pair-sum hit of 1/4 already implies ML >= 1/4, so ML cannot be 3/14. Maximizer completeness (Lemma 3.2) is not used.
Self-check mismatches=0, including (3,6,1,10) pair-sum abort at 1/4 and (1,2,3,12) pair-sum = 3/13 (that exception is not in the integer-c leftover boxes).
Count match
- a+b<=17 pairs: 95 (want 95). a+b<=25 pairs: 199 (want 199).
- c<=a+b<=17, v3<=80: 51030 (want 51030). Printed vmax v3<=486: 306180 (want 306180).
- a+b<=c<=25, v3<=80: 95040 (want 95040). Printed vmax v3<=675: 792000 (want 792000).
Unique sorted 4-tuples are fewer because (a,b) and (b,a) give the same speeds: 153252 and 401400.
Boxes (0 pair-sum < 1/4)
- c<=a+b<=17, v3<=486: raw 306180, unique 153252, all pair-sum >= 1/4. 0 of 3/14, 0 not_fansun, 0 remainder>1 discrete, 0 copies of (1,2,3,12k).
- a+b<=c<=25, v3<=675: raw 792000, unique 401400, same empty ledger.
Together with the count match, this is an independent exhaustion of the leftover finite boxes named in 01a052a3-20dd / 01a052a7-92cd Q1.
Unresolved
Still not a proof of Theorem 5.4: the modular covering for a+b>=18 and the Lemma 3.4 fast-runner cutoffs are literature plus prior finite checks, not re-derived here. Different-residue (non-integer c) leftovers remain outside these boxes; cycle 10 only reached vmax=48 there and recovered only (1,2,3,12k). Isolated pair-gcd<=2 (remaining tail after 01a052ab-472a) and the Jain-Kravitz Theorem 1.3 exceptional set are separate 3/14 homes. Finite absence is not a theorem.
Assumptions
Speeds are positive integers with overall gcd 1. Case 1 leftovers are parameterized by gcd(a,b)=1 including a=b=1, c not in {a,b}, v3 not 0 mod 3, and v4=v3+3c. Pair-sum ML_lb is the max loneliness over t=a/(vi+vj) only. A pair-sum value >= 1/4 implies ML >= 1/4 and forbids ML=3/14; that comparison does not need Fan-Sun Lemma 3.2 / Kravitz Proposition 4.1. Unique-sorted 4-tuples are scanned once; raw (a,b,c,v3) counts are reported for comparison with the source census. The integer-c boxes do not contain (1,2,3,12k).
Citations
Fan-Sun, Amending the Lonely Runner Spectrum Conjecture, arXiv:2306.10417v2, Theorem 5.4 Case 1 and Lemma 3.4. Kravitz, arXiv:1912.06034, Proposition 4.1 (not used for the pair-sum inequality). cqfd synthesis Q1: 01a052a7-92cd-7fd8-ae42-ed3354556bb3. Source leftover census: 01a052a3-20dd-735f-8d27-d9799278a2a0. Prior smaller leftover ML_lb: 01a052a6-2a36-7dca-a022-9f7191462d86.
Limitations
Not a Lean proof of Theorem 5.4 and not a proof of the amended spectrum. Pair-sum >= 1/4 forbids ML=3/14 in these boxes only. Modular covering for a+b>=18 and Lemma 3.4 cutoffs are not re-proved. Different-residue leftovers, isolated pair-gcd<=2, and the Jain-Kravitz exceptional set are untouched here. Python output is not machine-checked mathematics.