Mathematical remark

Partial writeup of Kravitz Lemma 7.1 residue casework, targeting conjecture version 01a05225-c3ac-7b0d-a93f-3ed77bdc84f8. Classification: reconstructed casework plus elementary D-mod-3/6 identities and finite residue checks. Not a Lean proof of Lemma 7.1, and not a proof of Theorem 7.2. This fills the gap recorded in partial_result 01a05287-2814-74b4-886d-10598e061507.

Claim

Let v1,v2,v3 be positive integers with overall gcd 1 and every pairwise gcd ≤ 2. Write D=v1+v2, r=⌊D/3⌋, and let L be the maximum of min_i ||t vi|| over t=m/D. If v3 is a multiple of D then L=0. Otherwise L≥r/D.

Always ||t v1||=||t v2|| at these times. Write D=3r, 3r+1, or 3r+2. Reduce the residue j of uv3 to 1≤j≤⌊D/2⌋ by replacing v3 with cD−v3 if needed.

gcd(v1,v2)=1 (1/6 D estimates removed)

Choose u with uv1≡1 (mod D) and reindex m≡ℓu. Then ||t v1||=||ℓ/D|| ≥ r/D for ℓ∈[r,D−r]. Need some such ℓ with ℓj mod D ∈ [r,D−r].

1. j=1: r·j ≡ r.
2. 2≤j≤D−2r+1: incrementing ℓ cannot skip [r,D−r], because if ℓj < kD+r then (ℓ+1)j ≤ (k+1)D−r. The unwrapped span is (D−2r)j ≥ 2(D−2r) ≥ 2r > 2r−2, so the values cannot sit in any interval [kD−r+1, kD+r−1].
3. D−2r+2 ≤ j < D/2. This range is empty unless (D,r) is (3r,r≥5), (3r+1,r≥6), or (3r+2,r≥7); first nonempty D are 15, 19, 23. Hideouts for pairs (ℓ,ℓ+1) with ℓ∈[r,D−r−1] are I1=[D−r−j+1,r−1] and I2=[D−r+1,D+r−j−1], with length-differences L1=2r+j−D−2 and L2=2r−j−2. L1<j because 2r<D+2; L2<j because j>r−1 (j≥D−2r+2 and D−3r+3≥3). So consecutive residues cannot stay in one Ii. Alternating puts at least N=⌊(D−2r)/2⌋ residues in I1, an AP of step h=D−2j≥1. Need (N−1)h>L1. Decreasing j increases h by 2 and decreases L1 by 1, so the worst case is j=⌊(D−1)/2⌋, which holds in all six (D mod 3, D parity) classes (e.g. D=3r, r odd: N−1=(r−3)/2, h=1, L1=(r−5)/2). This replaces the paper’s 1/6 D estimates, which are not valid for every D≥2 and are unused for D<15 because the range is empty.
4. j=D/2 (D even): r·j or (r+1)·j is ≡ D/2, and r≤D/2≤D−r.

gcd(v1,v2)=2 (sketches written out)

D is even. v3 is odd. Choose u with uv1≡2 (mod D). Even m become ℓ∈{1,…,D/2} with ||t v1||=||2ℓ/D|| ≥ r/D iff ℓ∈[⌈r/2⌉, ⌊(D−r)/2⌋]. Need some such ℓ with ||t v3|| ≥ r/D or ||t v3|| ≤ 1/2−r/D. The second suffices: v1,v2 even so t↦t+1/2 preserves those two distances, while v3 odd gives ||(t+1/2)v3||=1/2−||t v3||. (Printed “t1” is t.) Equivalently ℓj mod D lies in T=[r,D−r]∪[0,D/2−r]∪[D/2+r,D). The complement is J1=[D/2−r+1,r−1] and J2=[D−r+1,D/2+r−1], each of length-difference J=2r−D/2−2.

If J<0 (even D∈{2,4,6,8,10,14}) then T=ℤ/Dℤ and any ℓ works.

1. 1≤j≤D−2r+1 and J≥0. From r−1, adding j lands at most at D−r, so the AP cannot skip [r,D−r]. From the top of J2, adding j wraps to at most D/2−r. For D=6k, 6k+2, 6k+4 the pair (N,J) is (k+1,k−2), (k+2,k−3), (k+1,k−2), so (N−1)j ≥ N−1 > J. Thus the AP cannot sit in one J.
2. D−2r+2 ≤ j ≤ D/2−2, so h:=D−2j≥4. Now j may skip a single component of T, but consecutive terms still cannot stay in one J (J<j). Alternating puts at least N_even=⌊N/2⌋ terms in one J as an AP of step h. On the nonempty third-type range (k≥3) one has (N_even−1)·4 > J in each D mod 6 class. This is the paper’s “same as the third bullet, except h≥2 because D is even”, with the h=2 line removed.
3. j=D/2−1 (the h=2 line). Take ℓ=⌊(D−r)/2⌋. Then the residue is 4k=D−r if D=6k; k if D=6k+2; k+1 if D=6k+4. All three lie in T.
4. j=D/2: ℓ·j ∈ {0,D/2} ⊂ T (0 uses t+1/2).

Finite checks

Script: work/code/kravitz_lemma71_check.py. Plan: work/notes/kravitz_lemma71_formalization.md. No paper or repository code executed.

Residue hitting, D≤120: gcd=1, all j∈[1,⌊D/2⌋], 3600 pairs, 0 misses; even D gcd=2, 1830 pairs, 0 misses. Identities D≤200: third-range emptiness; I1,I2<j; both gcd=1 spans; gcd=2 bullet-1 span; h≥4 span; named j=D/2 and j=D/2−1 witnesses. 0 failures. Lemma statement on triples with some pairwise gcd exactly 2: vmax=36, 1293 triples, 0 failures.

Lean plan (unchecked)

Replay the four gcd=1 bullets and the five gcd=2 bullets as a standalone lemma, using only D=3r|3r+1|3r+2 and the t+1/2 identity. Then return to Theorem 7.2. Prop. 4.1 (ε; f=0) remains the largest gap for identifying ML with max L_{i,j}.