Mathematical remark

Partial replay of Fan–Sun n=4 large-gcd theorems as a checkable plan. Target: conjecture version 01a05225-c3ac-7b0d-a93f-3ed77bdc84f8. Classification: reconstructed proof plan plus finite exact-arithmetic checks. Not a Lean proof of Theorems 5.3/5.4, and not a proof of the amended spectrum.

Claim (Theorem 2.3 / 5.3 / 5.4 / Prop. 5.1)

Let v1,v2,v3,v4 be positive integers with overall gcd 1.

• If some pair has gcd g>3, then ML ≥ 1/4 (Theorem 5.3; repeats allowed).
• If some pair has gcd exactly 3, then ML ≥ 1/4 unless the speeds are a permutation of (1,2,3,12k) (Theorem 5.4 is printed with v1<v2<v3<v4 and exception (1,2,3,12k); the proof drops the order immediately).
• ML(1,2,3,12k)=3k/(12k+1), which is Kravitz form s/(4s+1) with s=3k (Prop. 5.1).

So every n=4 tuple with a pair-gcd ≥ 3 is either in the continuous region ML ≥ 1/n or on a remainder-1 discrete family. Pair-gcd ≤ 2 is not treated here.

Hidden comparisons

Theorem 5.1 (n≥4): if n-1 speeds share gcd g≥2, overall gcd is 1, and LRC holds for those n-1 speeds, then a pre-jump plus pigeonhole gives ML ≥ 1/2-1/(2g). The printed text writes ≥ 1/n directly. The comparison holds for every n≥4 and g≥2, because the left side is minimized at g=2 and equals 1/4 ≥ 1/n. For n=4 this uses only classical LRC for three speeds.

Lemma 5.1 reduces to: g≥6, z ≢ 0,±1 (mod g), and for every (a,b) on the torus some k has {a+k/g} and {b+kz/g} both in [1/4,3/4]. The paper’s “2k-1 valid points” count is a sketch; this covering statement is the claim used below.

Typo: the 5.3 bullet “breaks down when |v3-v4|=v3” means =v1.

Printed fast-runner cutoffs are conservative. Lemma 3.4 with L=1/3 and v_{n-2}≤54 gives v3≥486, not 1944. For the g=5 leftover, Lemma 3.4 gives b≥360, not 1440.

Case tree for 5.3 (gcd(v1,v2)=g>3; else permute. If v3 or v4 shares a factor with g, use 5.1)

1. v3 ≢ ±v4 (mod g), g≥6: LRC(n=2) on (v1,v2), then Lemma 5.1 on the pre-jump.
2. v3 ≡ ±v4, |v3-v4| not in {v1,v2}, g>3: need ||t(v3-v4)|| ≤ 1/2-1/g. Shifted LRC (Theorem 5.2) on (v1,v2,|v3-v4|) with starts (0,0,1/2) gives distance ≤ 1/4, and 1/4 ≤ 1/2-1/g for g≥4.
3. Same congruence, |v3-v4| in {v1,v2}, g≥6: after reducing gcd(v1,v2) to 1 the shifted speeds are (v1,v2,v1). Target ||tv1+1/2|| ≥ 1/g together with min(||tv1||,||tv2||)≥1/4. Explicit for v1=1; pre-jump 1/v1 for v1>1.
4. g=4: every coprime residue pair is ≡ ±. Leftover family (4,4a,b+4,b). For v3≥6, Lemma 5.1 plus a 4-pre-jump. Named leftover (4,4a,5,1): Lemma 3.3 for a>3.
5. g=5, ≡ ±: leftover (5,5k,b+5,b) with k≤8 and b up to the printed 1440, claimed computer-checked in the source.
6. g=5, not ≡ ±: force three valid h at t=(2k+1)/(4v3), then Lemma 5.1 at modulus 2v3/min(gcd(2v3,v1),gcd(2v3,v2)). The min-gcd is ≤3 else a pair-gcd ≥4 was already treated. Needs v3≥9; v3<9 is residue casework, and {2,3} reduces to v4=1 and LRC(n=3) on (v1,v2,5).

Theorem 5.4 Case 1 (difference not equal to v1 or v2) uses the same 1/6-distance target and bounds a+b≥18 or c≤25, leaving v1,v2<54 or ≤75 plus fast-runner cutoffs. Case 2 is not replayed this cycle.

Finite checks (work/code/fan_sun_n4_check.py; exact rationals; 0 failures)

• Theorem 5.1 comparison n=4…20, g=2…40.
• Lemma 5.1 count 3*floor(g/2)-1>g for g=6…80.
• Lemma 5.1 covering on the critical-line arrangement, g=6…24, all z=2…g-2: 161175 cells, 0 misses.
• Theorem 5.4 counting: 2(floor(m/2)-1)/m ≥ 2/3 for m=8…200; floor(m/2)-1 > m-2*floor(m/3) for m=18…200.
• Prop. 5.1: ML_lb(1,2,3,12k)=3k/(12k+1) for k=1…30, all strictly below 1/4.
• Named g=4 leftovers: ML_lb(4,8,5,1)=1/3 and ML_lb(4,12,5,1)=1/4; also a=1 and a=4…10 all ≥ 1/4.
• n=4 box vmax=16, nondecreasing, overall gcd 1: 2164 tuples with some pair-gcd>3, 0 below 1/4; 490 with max pair-gcd=3 including one exception (1,2,3,12), 0 non-exception below 1/4.
• g=5 leftover slice k=1…8, b=1…40: 256 gcd-1 tuples, 0 below 1/4.

Gaps left

Lemma 5.1 covering is complete only for g≤24, not a general proof. Theorem 5.2 is unused as a derivation. The source’s g=5 b≤1440 box and the Theorem 5.4 leftover boxes are not independently exhausted. Prop. 5.1 still depends on maximizer completeness for the “only these denominators” step. Lean is not installed.