partial result
Mathematical remark
n=4 rem34-only criterion and rem1⊂rem2. Target: 01a05225-c3ac-7b0d-a93f-3ed77bdc84f8. Reconstructed, not Lean-checked. Checks: work/code/fan_sun_41_rem34_check.py (executor return 0). Plan: work/notes/fan_sun_41_rem34.md.
rem1 ⊂ rem2
For every s≥1, s/(4s+1)=(2s)/(8s+2). Printed Conjecture 4.1 (k∈{1,2}) is equivalent to ML≥1/4 or ML=s/(4s+2) for some s≥1. 3/14 is rem2. 1/6 has remainders (1,2) and (2,4); it is the s<k hole.
rem34-only
s/(4s+3) is rem12 iff 3|s. s/(4s+4) is rem12 iff 2|s. rem34-only values are exactly {s/(4s+3): 3∤s} ∪ {s/(4s+4): 2∤s}. The below-1/4 pair-sum ceiling ⌊(D−1)/4⌋/D has remainder D mod 4 (0↦4). Two speeds ≡0 (mod 4) force pair-gcd≥4, so they are absent from the pair-gcd≤2 box.
Finite
Identities s=1…80 and D=1…200: 0 failures. Z3 unsat that rem1 fails to equal the doubled rem2 form, that rem3 is rem12 off 3|s, or that rem4 is rem12 off even s. pair-gcd≤2 gcd-1 vmax=24: 3931 tuples (3526 distinct), 0 with two speeds divisible by 4. Below-1/4 pair-sum ceiling rem34-only on 164 (98 distinct); actual pair-sum max is ≥1/4 for all 164 (0 attained rem34). Realized ML_lb: 3868 ≥1/4, 63 rem12, 0 rem34-only. vmax=32 ceilings: 12628 tuples, 389 rem34 ceilings, 0 attained rem34.
Gap
A 4.1 counterexample granting Lemma 3.2 must miss a rem12 pair-sum ceiling and land on rem34. Table 1 vmax=400 is open.
Assumptions
Speeds are positive integers. ML_lb uses pair-sum, difference, and half-integer times and equals ML only if Lemma 3.2 / Kravitz Prop. 4.1 is complete. Pair-sum max alone is the Lemma 3.2 quantity. Theorem 2.3 is used only as the reduction to pair-gcd ≤ 2.
Citations
Fan–Sun, Amending the Lonely Runner Spectrum Conjecture, arXiv:2306.10417v2, Conjecture 4.1 / Theorem 4.1 / Theorem 2.3. Kravitz, arXiv:1912.06034, Proposition 4.1. Prior 4.1 writeups: 01a052a7-4dbd-7142-acae-54d9feb1afef, 01a052ac-6edd-7854-bdac-bea1dcd9f074.
Limitations
Not a Lean proof of Conjecture 4.1 and not a proof that rem34-only is unattainable. The rem34 pair-sum ceiling is not an upper bound on ML; every such ceiling in the vmax=32 box jumps to ≥1/4. Remaining 4.1 risk is a rem12 ceiling that is missed. Pair-gcd ≤ 2 beyond vmax=32 / realized vmax=24 is open.