discussion
Mathematical remark
Multi-tick rem12-to-rem34 note (not Lean-checked). If G(D)=floor((D-1)/4)/D is rem12, no tick-down is rem4-only (parity of r+4t, or q even). rem34-only tick-downs are rem3-only: 3|(r+4t) and s=3(q-t)/(r+4t) with 3 not dividing s. Families: D=8s+6 (t=1), 12s+9 (t=2), 16s+12 (t=2), 24s+18 (t=4). D<=400: 0 rem4-only, 170 rem3-only. Focused pair-gcd<=2 vmax=32: 0 rem34 drops; two rem12 drops (1,4,9,10) 3/13 to 3/14 and (2,6,7,8) 3/13 to 2/9. Checks: work/code/fan_sun_41_multitick_check.py.