Mathematical remark

Partial replay of Fan–Sun Theorem 5.4 Case 1, 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 1 is: gcd(v1,v2)=3, v3 and v4 coprime to 3, |v3-v4| not in {v1,v2}, overall gcd 1. Write a=v1/3, b=v2/3, c=|v3-v4|/3, and reduce to gcd(a,b)=1 (else a pair-gcd >3 and Theorem 5.3 applies). Need min(||t v1||, ||t v2||) ≥ 1/4 and ||t(v3-v4)|| ≤ 1/6.

Hidden rescaling: after τ=3t this is min(||τ a||, ||τ b||) ≥ 1/4 and ||τ c|| ≤ 1/6. The paper’s times t=ℓu/(a+b) are τ-times.

The printed exception (1,2,3,12k) is Case 1 before the sign flip that forces v3 ≡ v4 (mod 3). After that flip the difference becomes 1+2=3=v1, i.e. Case 2. The integer-c leftover boxes below therefore do not contain this family; §5.5 is correct that Lemma 3.3 then divides by zero because ML(1,2,3)=1/4.

Subcase c ≤ a+b

Times τ=ℓu/m with m=a+b and au≡1 (mod m). Then ||τ a||=||ℓ/m|| and ub≡-1, so ||τ b||=||ℓ/m||. Residue z=uc (mod m).

• z=0: ||τ c||=0. Any ℓ with ||ℓ/m||≥1/4 works.
• z=1 is c=a; z=-1 is c=b. Both are Case 2 and are excluded. On m=18…80 those two residues never hit L0 among valid ℓ (126 checks, 0 hits).
• 2≤z≤m/3: need 2(⌊m/2⌋-1)/m ≥ 2/3. Holds for every m≥8 (m≤400; eventual threshold exactly 8).
• m/3<z<m/2: L0={p : ||p/m||≤1/6} has |L0|=2⌊m/6⌋+1 ≥ ⌊m/3⌋ (m≤400, 0 bound failures). Printed pigeon ⌊m/2⌋-1 > m-2⌊m/3⌋ holds for every m≥18 (eventual threshold exactly 18; no Case-2-style equality failures). Exact |L0∪L1| also has 0 pigeon misses for m≥18.
• z=m/2: ||ℓz/m||=||ℓ/2|| is 0 or 1/2. Any even ℓ in [m/4, 3m/4] works, and exists for every even m≥4. The printed ℓ=⌊(g+1)/2⌋ reads g for m; it fails only at m=2, which is leftover anyway.

Modular covering after excluding z≡±1: m=18…80, 2961 residues, 0 misses. Combined leftover is a+b≤17, hence v1,v2<54.

Fast-runner cutoffs

Lemma 3.4 with L≥1/3 and vn-2≤54 needs v≥486, not the printed 1/(1/3-1/4)·3·54=1944 (Lemma 3.3 shape with an extra factor 3). For the c≥a+b leftover, vn-2≤75 needs v≥675. Because c≤a+b≤17 forces |v3-v4|<54, the two large speeds cannot split: if min(v3,v4)<486 then both are <540. The printed “v3 small, v4 huge” Lemma 3.3 branch does not occur here.

Subcase c ≥ a+b

Times τ=k/c force ||τ c||=0. If Lemma 5.1 fails then max(A,B)≤5, so c≤A·B≤25 and a+b≤25, hence v1,v2≤75. Same finite leftover with |v3-v4|≤75.

Finite leftover (explicit pair-sum times; does not need maximizer completeness)

WLOG v3<v4. All gcd-1 tuples with v3,v4 coprime to 3:

• c≤a+b≤17, v3≤486: 306180 tuples, 0 below 1/4, 0 exceptions.
• a+b≤c≤25, v3≤675: 792000 tuples, 0 below 1/4, 0 exceptions.

Together with the Case 2 leftover already checked, every n=4 pair-gcd=3 configuration outside (1,2,3,12k) reaches 1/4 at an explicit pair-sum time in these boxes, or is covered by the repaired modular / Lemma 3.4 arguments above.

Limits

Not a Lean proof of Theorem 5.4. The shifted pre-jump that turns ||t(v3-v4)||≤1/6 into ML≥1/4 is taken from earlier Fan–Sun sections. Pair-gcd ≤2 remains Fan–Sun Conjecture 4.1. No paper or repository code was executed. Python output is not machine-checked mathematics.