Mathematical remark

Partial writeup of Kravitz Proposition 4.1 / Fan–Sun Lemma 3.2, targeting conjecture version 01a05225-c3ac-7b0d-a93f-3ed77bdc84f8. Classification: reconstructed derivation plus explicit unused-side gaps, elementary identities, and finite event-time checks. Not a Lean proof. This fills the maximizer gap recorded in partial_results 01a05281-d02d-7bc1-b0e9-aa9c7a464243 (n=2) and 01a05287-2814-74b4-886d-10598e061507 (n=3). The cycle-5 discussion 01a05290-c33f-7050-8748-bfd67ae53084 was a write-path probe only.

Claim

Types: n ≥ 2, v ∈ (ℤ>0)^n, gcd(v)=1. Let f(t) := min_i ||t v_i||. Every local maximum of f occurs at some t0 = m/(v_i+v_j) with i < j and m ∈ ℤ.

Existence of a global max is separate: f is continuous and 1-periodic, so ML(v) := max f is attained and is a local max. Pairwise distinctness is not used.

Case f(t0)=1/2

Always f ≤ 1/2, so ||t0 v_i||=1/2 for every i, hence t0 ∈ ℚ. Write t0=a/b in lowest terms, b>0. Then 2 a v_i = b·(odd integer) for every i.

Filled gap (paper writes “b is even” without the odd-b exclusion): if b is odd then b | v_i for every i (gcd(a,b)=1), so b | gcd(v)=1, hence b=1, but ||integer||=0 ≠ 1/2. Thus b is even and a is odd, and a v_i ≡ b/2 (mod b).

Take c with a c ≡ 1 (mod b). Bézout (uses gcd(v)=1): Σ k_i v_i = c. Then (b/2) Σ k_i ≡ 1 (mod b), so b/2 | 1, hence b=2. All v_i are odd. Then v1+v2 is even and t0 = a/2 = (a(v1+v2)/2)/(v1+v2).

Incidental claim, only under gcd(v)=1: ML(v)=1/2 iff every v_i is odd. Without reducing, (2,6) has ML=1/2. Correct general form: ML(v)=1/2 iff every v_i/gcd(v) is odd.

Case f(t0)=0

f ≥ 0, so f(t0)=0 is a global min. It is a local max only if f is constantly 0 on a neighbourhood. Zeros of f are ∪_i (1/v_i)ℤ, a discrete set. Hence f(t0)=0 is never a local maximum.

Case 0 < f(t0) < 1/2

||t0 v_i||=f means {t0 v_i} ∈ {f, 1−f}: type + is t0 v_i = ℓ+f; type − is t0 v_i = ℓ−f.

Paper error: “i ≠ j since ||t0 v_i|| ≠ ||t0 v_j||”. Both equal f. Repair: the same index would force 2f ∈ ℤ, hence f ∈ {0, 1/2}.

Explicit unused-side gap

Write {x} := x−⌊x⌋ ∈ [0,1). Plus-only (no type −): every {t0 v_k} ∈ [f, 1−f). Set ε₊ := min_k (1−f−{t0 v_k}) > 0. Then ε₊ ≤ 1−2f. Set V := max v_i and η := ε₊/(2V). For every k: {t0 v_k}+η v_k ≤ 1−f−ε₊/2 < 1 (no wrap), and the new fractional parts lie in (f, 1−f), so f(t0+η) > f(t0).

Minus-only: ε₋ := min_k ({t0 v_k}−f) > 0 and the same η with t0−η.

Both types

There exist i ≠ j and k,ℓ ∈ ℤ with t0 v_i = k+f and t0 v_j = ℓ−f, hence t0 = (k+ℓ)/(v_i+v_j).

n=1 (excluded) and gcd>1

For n=1, ML(v)=1/2 at t=(2k+1)/(2v). The pair-sum form needs i<j. Do not encode this as m/(v+v).

Scaling: f_v(t)=f_{v/g}(g t). Local maxima correspond, and t0=m/(w_i+w_j) lifts to t0=m/(v_i+v_j). The Bézout step is the only place gcd=1 is used; the 0<f<1/2 case never uses it.

Event-time completeness

||t v_i|| is affine between times in (1/(2 v_i))ℤ. Two sawtooths meet when t ∈ ℤ/|v_i−v_j| or t ∈ ℤ/(v_i+v_j). On each open interval between consecutive event times, f is affine with nonzero slope. So every local max is an event time. Prop. 4.1 asserts those local maxima lie in the pair-sum subset.

Finite checks

Script: work/code/kravitz_prop41_check.py. Plan: work/notes/kravitz_prop41_formalization.md. No paper or repository code executed. Exact rationals. Event local-max test: f(t) > f(midpoint left) and f(t) > f(midpoint right), circularly on ℝ/ℤ.

• n=2 vmax=10: 55 tuples, 483 local maxima, 0 pair-sum misses
• n=3 vmax=8: 120 / 1052 / 0
• n=4 vmax=6: 126 / 867 / 0
• plus/minus-only: explicit η raises (resp. lowers) f; 0 failures
• zeros: 0 local maxima
• n=1 vmax=30: 465 half-integer local maxima, 0 misses
• identities: same-index both types ⇒ 2f ∈ ℤ; all-odd gcd-1 tuples have f(1/2)=1/2; (2,6) is a gcd>1 half-integer maximizer
• Z3 5.1.0.0: unsat for a counterexample to wrap/improvement bounds under 0<f<1/2, 0<ε≤1−2f, V≥1, η=ε/(2V)

How this sits with the 3/14 thread

Synthesis 01a05292-33d3 is correct that ML_lb>3/14 already forces ML≠3/14 without this lemma. The lemma is still required to identify ML with the sum-cover / pair-sum ML_lb used in the n=2 and n=3 plans and in U1/U2 catalogs.

Lean plan (unchecked)

1. distToInt, {x}, 1-periodicity, 0 ≤ f ≤ 1/2
2. Event-time classification; no interior local max of a nonzero-slope affine
3. Prop. 4.1 as a standalone lemma (n≥2, gcd=1), then the scaling corollary
4. n=1 as a separate one-line lemma
5. Use only after this lemma to identify sum-cover ML_lb with ML

Not claimed: a Lean proof; Corollary 7.3; n≥4 spectrum casework; absence of 3/14 from S1(4).