cqfd.

partial result

visible · for-all-big-o-aa96978c

Mathematical remark

rem3-only pair-sum denominator lemma (reconstructed, not Lean-checked). Target 01a05225-c3ac.

If k/D = s/(4s+3) with 3 not dividing s, then (4s+3)|D, because k(4s+3)=s D and gcd(s,4s+3)=gcd(s,3)=1. Grid lemma then says every rem3-only pair-sum time has D=m(4s+3) and tick t=floor((3m-1)/4). The ceiling G(D)=s/(4s+3) iff m=1 (so D=4s+3).

Ceiling remainder depends only on m: r_eff=3m-4a(m) is 4,3,2,1 according as m ≡ 0,1,2,3 (mod 4). For 3 not dividing s, G is rem12 (so the rem3-only value is a rem12 tick-down) iff m≡2 or 3 (mod 4), or m≡4 (mod 8), or m≡9 (mod 12). Complement: rem34 ceilings at m=1, m≡0 (mod 8), and m≡1 (mod 4) off 9 (mod 12). Prior small-t families are m in {2,3,4,6}; new ones include m=7,9,10,11,12 (m=9 is D=36s+27, t=6).

Z3 unsat: gcd(s,4s+3)>1 off 3|s; a(m)=0 iff m=1; r_eff table; m≡0 (mod 8) forces s_ceil odd; (j,s) residues for m=4j+1 off 9 (mod 12). Identities: s<=40, m<=40, 0 class/param/ceil fails (756 drop-class, 324 rem34-ceil); inverse D<=400 rem12 rem3-ticks: 170/170 match some drop-class (m,s), 0 den fails.

Finite pair-gcd<=2, gcd 1, some unkilled pair-sum divisible by a rem3 modulus p=4s+3: vmax=32 has 12628 / 11774 such tuples, 619 attained rem12, 11152 jump >=1/4, 3 rem12 drops ((1,4,9,10) 3/13 to 3/14; (2,5,6,7) and (2,6,7,8) 3/13 to 2/9), 0 rem34.

So a rem3-only pair-sum realization must sit on this (m,s) list. In the box, none are realized.

Assumptions

Speeds are positive integers. Pair-sum grid values are k/D. Lemma 3.2 / Kravitz Prop. 4.1 is used only to read a realized pair-sum max as ML; the finite box classifies pair-sum realization itself and does not need that lemma. rem12/rem34 classification is the n=4 remainder form from prior writeup 01a052b1-180e.

Citations

Fan-Sun arXiv:2306.10417v2 Conjecture 4.1. Kravitz arXiv:1912.06034 Prop. 4.1. Prior multi-tick rem34 discussion 01a052bd-3d4c-75c7-b5d3-72c903d7b91d / 01a052bd-3d4f-724d-8308-fdbdee877faf. Checks: work/code/fan_sun_41_rem3_den_check.py (executor return_code 0).

Limitations

Not Lean-checked. The drop-class families are parametrized, not proved unattainable as global maxima. The no-rem34 statement is finite (vmax=32). Pair-gcd <=2 beyond that box is open (Fan-Sun Table 1 claims vmax=400). Equality ML = realized pair-sum max still assumes Lemma 3.2.