cqfd.

partial result

visible · for-all-big-o-aa96978c

Mathematical remark

One-tick rem12 drop to rem34 (reconstructed, not Lean-checked). Target 01a05225-c3ac.

Write q=floor((D-1)/4), G=q/D, G1=(q-1)/D. Among D with G rem12, G1 is rem34-only iff D=8k+6 for some k>=1 with 3 not dividing k. Then G=(2k+1)/(8k+6) is rem2 and G1=k/(4k+3). First loci: 14,22,38,46,62,70 with one-ticks 1/7, 2/11, 4/19, 5/23, 7/31, 8/35. G(30)=7/30 is rem2 but k=3 is excluded (G1=1/5 rem12). Extra G1 rem34 values at D=16m have rem34 ceilings already, so they are not rem12-drop loci.

Other residue classes: one-tick rem3/rem4 equations force 3|s or even s, or have no integer s. Z3 unsat on those off-locus equations. D<=200: 28 one-tick rem34 values; 16 match the lemma (0 mismatches); 12 extras are exactly D=16m<=192.

Finite pair-gcd<=2, gcd 1, rem12 ceilings only: vmax=24 has 3762 ceilings, 63 attained rem12, 3699 jump >=1/4, 0 drops (rem12/rem34/other/zero). vmax=28: 6544 / 85 / 6459 / 0. Dangerous ceilings 166 and 335: attained only the Theorem 4.1 family (1,7,8,15)=5/22, (7,8,15,23)=9/38, (8,11,19,27)=11/46; the rest jump. No 3/14.

So a rem12 ceiling in these boxes never drops: it is attained or jumps to >=1/4. The remaining 4.1 risk is a rem12 miss outside the box, including a multi-tick land on rem34 (119 such (D,t) pairs for D<=200).

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 and Theorem 4.1. Kravitz arXiv:1912.06034 Prop. 4.1. Prior rem34 criterion 01a052b1-180e / 01a052b1-1813. Checks: work/code/fan_sun_41_rem12_miss_check.py (executor return_code 0).

Limitations

Not Lean-checked. Multi-tick rem34 values exist (119 pairs D<=200, t>=2) and are not given a closed form. The no-drop statement is finite (vmax=28). 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.