Mathematical remark

Partial replay of Fan–Sun Theorem 5.4 Case 2, with independent leftover checks. Target: conjecture version 01a05225-c3ac-7b0d-a93f-3ed77bdc84f8. Classification: reconstructed proof plan plus finite exact-arithmetic checks. Not a Lean proof, and not a proof of the amended spectrum.

Claim

After dropping the printed order, Case 2 is: gcd(v1,v2)=3, v3 and v4 coprime to 3, |v3-v4|=v1 (or v2 by swapping), overall gcd 1. Then ML≥1/4. The printed exception (1,2,3,12k) is not in this case: its only pair-gcd equal to 3 is (3,12k), and |1-2|=1 is not in {3,12k}. That family lives in Case 1, where Lemma 3.3 divides by zero because ML(1,2,3)=1/4.

Write a=v1/3, b=v2/3, c=v3, and reduce to gcd(a,b)=1 (else a pair-gcd >3 and Theorem 5.3 applies).

Why the 1/6 target fails, and the repair

Case 1 wants ||t(v3-v4)||=||t v1||≤1/6 together with ||t v1||≥1/4, which is impossible. The paper instead forces runner 3 into a 1/12-neighborhood of a multiple of 1/3, equivalently ||t(3v3)+1/2||≥1/4. Because v3 is coprime to 3, the three pre-jump positions are {x,x+1/3,x+2/3}; exactly two then satisfy ||·||≥1/4. The difference t(v3-v4) is invariant under t↦t+h/3. A one-sided shift of size ≤1/3 keeps at least one of those two valid, so it is enough to find t with

min(||t v1||, ||t v2||, ||t(3v3)+1/2||) ≥ 1/4 and ||t v1|| ≤ 1/3.

Hidden rescaling: the paper’s later (a,b,c) form is the same claim after τ=3t. Times t=k/v1+p with p in [1/(4v1),1/(3v1)] force ||t v1|| in [1/4,1/3].

Bounding a, then c

(1) If c is a multiple of a then v4 is too; a>2 gives Theorem 5.1. (2) If c ≢ ±b (mod a) and a≥6, Lemma 5.1 applies. (3) If c≡±b (mod a) and c≠b, the interval t in [1/(4a),1/(3a)] sweeps an arc of length ≥1/12 for t(b-c)+1/2, hence min ||x+1/2|| ≤ 1/2-1/24, which is ≤ 1/2-1/a iff a≥24. So a≥24 (i.e. v1≥72) is claimed, but this bounds only one speed.

To bound c, fix runner 3 at 1/4 and reduce the step by gcd(a,c)gcd(b,c)∈{1,2}. Set d=c/(that product) ≥ c/2. Casework on z≡ua (mod d), ub≡1:

• z=1: k=u(⌊d/4⌋+1) lands in [1/4,1/3]∪[2/3,3/4] for every d except {2,4,5,8}.
• 2≤z≤d/4: need 2(⌊d/2⌋-1)/d ≥ 3/4. Printed “d≥10” fails at d=11 (8/11<3/4). Holds for all d≥12.
• d/4<z<d/2, z≠d/3: printed |L0∪L1|≥2⌊d/4⌋+⌊d/12⌋ holds, but the pigeon using that bound fails at the equalities d=39,43,47 and only becomes uniform at d≥48. Smallest repair: use the exact |L0∪L1|. That pigeon has 0 failures for every d≥36.
• z=d/3 or d/2: the printed “a and b both multiples” is inaccurate; the intended Theorem 5.1 appeal is not re-proved here.

With the exact-union repair, d<36 still implies v3<72, hence v1,v3,v4<72.

Finite leftovers independently exhausted

Lemma 3.3 cutoff from ML_lb(v1,c,v4)>1/4: 552 Case 2 triples with a≤23 and c<72, 0 tight, cutoffs 28…490. Every eligible v2=3b up to the cutoff reaches 1/4 at an explicit pair-sum time (19411 tuples, 0 failures). This does not use maximizer completeness.

Source g=5 family (5,5k,b+5,b), k≤8. Lemma 3.4 with L≥1/3 and v_{n-2}≤40 needs b≥360, not the printed 1440. All gcd-1 tuples with b=1…360: 2304 tuples, 0 below 1/4, again by explicit pair-sum times.

Checks: work/code/fan_sun_54_case2_check.py. Plan: work/notes/fan_sun_54_case2_formalization.md.

Still open

Theorem 5.4 Case 1 leftover boxes (v1,v2<54 or ≤75, third/fourth speeds up to the fast-runner cutoffs) are not independently exhausted. Pair-gcd ≤2 remains Fan–Sun Conjecture 4.1. Lean is not installed.