Mathematical remark

Partial replay of Kravitz’s n=3 spectrum proof as a checkable plan, targeting conjecture version 01a05225-c3ac-7b0d-a93f-3ed77bdc84f8. Classification: reconstructed proof plan plus finite exact-arithmetic checks. Not a proof of Theorem 7.2 or of the amended spectrum. Lean is not installed.

Claim

Let v1,v2,v3 be positive integers with gcd=1 (repeats allowed). Then either ML(v)≥1/3 or ML(v)=s/(3s+1) for some s∈ℕ. This is Kravitz Theorem 7.2 and the n=3 case of both Conjecture 1.2 and the amended statement (only remainder m=1 occurs below 1/3). Scale to drop the gcd=1 hypothesis.

Dependency chain: Prop. 4.1 (maximizers) → Theorem 6.1 (n=2; pair-ML≥1/3) → Lemma 7.1 → Theorem 7.2 casework. Corollary 7.3 (only tight triple is 1,2,3 up to scaling) is a sketch in the source and is not claimed.

Hidden cases (filled)

(1) Two or three speeds ≡0 (mod 3). Three contradicts gcd=1. Two forces those two to have pairwise gcd ≥3, so the pre-jump applies. Finite: vmax=20, 249 gcd-1 triples with at least two multiples of 3, 0 exceptions to “some pairwise gcd ≥3”.

(2) Pairwise distinctness is not needed. Equal speeds ≥3 are pre-jump; (1,1,·) and (2,2,·) fall under Lemma 7.1.

(3) Collapse L=r/D. Lemma 7.1 gives only L≥r/D with r=⌊D/3⌋, D=vi+vj. Loneliness at denominator D lies in (1/D)ℕ. The next tick (r+1)/D is already ≥1/3, with equality iff 3|D. Hence under the standing restriction L<1/3, if 3∤D then L=r/D, and if 3|D the second dichotomy is disallowed. Identity: D≤300, 0 failures.

Pre-jump

If some pairwise gcd g≥3, say gcd(v1,v2)=g, then gcd(g,v3)=1. Theorem 6.1 gives t with ||tv1||,||tv2||≥1/3. The translates t+h/g fix those two runners. Residues of (t+h/g)v3 form a full 1/g-grid, so max_h ||(t+h/g)v3|| ≥ 1/2−1/(2g) ≥ 1/3, the last iff g≥3 (equality at g=3). Checked g≤200, 0 failures. Thus ML≥1/3.

Remaining: all pairwise gcd ≤2. If no speed is a multiple of 3, t=1/3 already gives loneliness 1/3. Remaining: exactly one speed ≡0 (mod 3).

Lemma 7.1 (largest remaining gap)

For a pair with D=v1+v2, r=⌊D/3⌋, L = max loneliness at t=m/D: if v3 is a multiple of D then L=0; else L≥r/D. Hypothesis: overall gcd 1 and no pairwise gcd >2, so gcd(v1,v2)∈{1,2}.

The gcd=1 half is written (four ranges for the residue of uv3). The gcd=2 half is explicitly a sketch (same interval logic plus a t ↦ t+1/2 pre-jump; printed “t1” is t). Smallest repair: write the gcd=2 bullets in full, and replace the 1/6 D estimates in the third gcd=1 range by inequalities valid for every D≥2.

Finite check of the lemma statement, not of the casework: vmax=28, overall gcd 1, pairwise gcd ≤2, 5015 triples, 0 failures (188 multiples of D, all with L=0).

Theorem 7.2 after the lemma

Prop. 4.1 ⇒ ML = max of the three L_{i,j}. If any L≥1/3, done.

All three pairs in the second dichotomy. Residues are (1,1,0) or (2,2,0).

• (1,1,0): v=(3a+1,3b+1,3c), a<b. Then L23=(b+c)/(3(b+c)+1) is strictly largest (cross-multiply). Checked a<b≤40, c≤40, 32800 triples, 0 failures. This is Kravitz form.

• (2,2,0): v=(3a+2,3b+2,3c), a<b. L12 is Kravitz form. L23>L12 iff c>2a+b+2 (13950 triples, 0 failures). In that branch the explicit time t=1/3−1/(9c) has loneliness ≥1/3 (0 failures). So either L12 wins or ML≥1/3.

Some pair in the first dichotomy, say v3 is a multiple of v1+v2, so L12=0.

• Both other sums ≡1 (mod 3): both remaining L are Kravitz form. • Mixed 1 and 2: the ≡1 value is larger, because 2q>p reduces to 2D13>D23, which holds under v3=k(v1+v2). • Both ≡2 (mod 3): then v1≡v2≡2 and v3≡0, and t=1/3−1/(3v3) has loneliness ≥1/3 (uses v3≥v1+v2>v1). Checked 61 instances with vmax=24, 0 failures.

Finite box for the theorem

Independent sum-cover ML_lb on gcd-1 nondecreasing triples, vmax=18: 915 triples, 0 values below 1/4, 0 values that are neither ≥1/3 nor of the form s/(3s+1). Split: 872 with ML_lb≥1/3; 43 discrete, all remainder 1.

Named ML_lb: (1,1,1)=1/2; (1,2,3)=1/4; (1,1,2)=(1,2,4)=(1,2,5)=(1,4,5)=(2,3,6)=1/3; (1,2,6)=2/7; (2,2,3)=(4,5,6)=2/5.

Script: work/code/kravitz_n3_check.py. Plan: work/notes/kravitz_n3_formalization.md. No paper or repository code executed.

Lean plan (unchecked)

Close Prop. 4.1 (ε; f=0). Replay Theorem 6.1. Write Lemma 7.1 with a complete gcd=2 case. Then Theorem 7.2 and AmendedSpectrum 3. Do not identify ML_lb with ML except after Prop. 4.1. n≥4 is not claimed.