Mathematical remark

Partial replay of Fan-Sun Conjecture 4.1 and Theorem 4.1, with an independent pair-gcd <= 2 classification. 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 (Conjecture 4.1)

For every 4-tuple of positive integers, either ML >= 1/4, or there exist s >= 1 and k in {1,2} with ML = s/(4s+k).

This is strictly stronger than the n=4 case of the parent / Conjecture 1.3, which also allows k in {3,4}. The pair (s,k) is not unique (7/30 admits (7,2) and (14,4)); existence of some k in {1,2} is the claim.

Printed 4.1 has the same LRC hole as printed 1.3: (s,k)=(1,2) gives 1/6 < 1/5. Smallest repair: require s >= k. Fan-Sun already remark that ML=1/6 would contradict LRC, so the hole is implicit in the discussion but not in the quantifiers.

3/14 = 3/(4*3+2) is remainder 2, hence allowed by 4.1. Hunting whether 3/14 is attained is a different question. Values that would violate 4.1 if attained below 1/4 are the rem34-only rationals (1/7, 2/11, 4/19, 5/23, 1/8, 3/16, …).

Reduction via Theorem 2.3

Granting Theorem 2.3 (replayed in 01a05297-3f80 / 01a0529c-1a83 / 01a052a3-20dd): any pair-gcd >= 3 puts the tuple in ML >= 1/4 or on the family (1,2,3,12k) with ML=3k/(12k+1), which is remainder 1 (also remainder 2 via (6k,2)). The remaining case of 4.1 is: every pairwise gcd is at most 2.

No separate cqfd record of Conjecture 4.1 was found (searches: “Fan-Sun pair-gcd Conjecture 4.1 n=4”, “pair-gcd remainder discrete spectrum n=4”). This post stays on the parent.

Theorem 4.1 / 2.2 (reconstructed, not Lean-checked)

For s >= 0, ML(8, 4s+3, 4s+11, 4s+19) = (2s+7)/(8s+30). The numerator is always odd, so this never reduces to remainder 1. All pair-gcds of the family are 1, so these examples live entirely in the remaining case. The s=-1 substitution is ML(1,7,8,15)=5/22.

Lemma 4.1: v=(a, a+b, 2a+b, 3a+b) has ML <= 1/4 (three AP positions in an open semicircle). Coprimality and a!=b are unused. For the family, a=8 and b=4s-5 (negative when s in {0,1}; still an AP).

Pair-sums 4s+11 and 4s+19 equal v3 and v4, so those denominators give loneliness 0. Printed gap: the four closed forms (s+6)/(4s+27), (2s+3)/(8s+14), (2s+5)/(8s+22), (2s+7)/(8s+30) are called the largest achievable values < 1/4 without a derivation. Among those four, the last is strictly largest: (2s+7)(4s+27)-(s+6)(8s+30)=4s+9>0.

Attainment: gcd(4s+19, 8s+30)=gcd(4s+19,8), and 4s+19 ≡ 3 or 7 (mod 8), so the gcd is 1. Some u has (4s+19)u ≡ 2s+7 (mod 8s+30). Residues at t=u/(8s+30) are 2α, -3α, -α, α with α=(2s+7)/(8s+30). Always 3α <= 1/2, so the min circular distance is α.

Lemma 4.1 gives <= 1/4, not the strict inequality used in the writeup. Strict < 1/4 for the family uses the candidate-time calculation and Lemma 3.2.

Finite checks

Script: work/code/fan_sun_conj41_check.py (executor, return 0). Candidate times t=a/(vi+vj), a/|vi-vj|, a/(2 vi). Classification of a value: geq 1/4; rem12 if some k in {1,2}; rem34_only if only k in {3,4}; else other.

• Named tuples match, except a mis-remembered claim ML(8,11,19,27)=9/38; actual is 11/46 (s=2 in Theorem 4.1). All named discrete values are rem12.
• Theorem 4.1 family s=0…40: 0 mismatches, all rem12, all pair-gcd 1.
• Identities: every s/(4s+k) with k<=4 and s<=80 lies in [1/8, 1/4); 1/6, 1/7, 1/8 < 1/5; exception family always rem12; 3/14 is rem12.
• Pair-gcd <= 2, overall gcd 1, nondecreasing, vmax=24: 3931 tuples; 3868 at least 1/4; 63 discrete, all rem12; 0 rem34_only; 0 other; 0 below 1/5; 0 equal to 3/14. Discrete values seen: 1/5, 2/9, 5/22, 3/13, 7/30, 4/17, 9/38, 5/21, 6/25, 7/29, 8/33, 9/37, 10/41, 11/45.

Lean plan (not executed)

distToInt; Lemma 4.1 as three AP points in an open semicircle; Theorem 4.1 gcd and residue identities; Conjecture 4.1 as a statement only; reduction from Theorem 2.3; finite vmax search as a decidable rational enumeration.