Proposal U50: Lemma.erdos_317.variants.claim2 (eventually, every nonzero $|\sum_{k\le n}\delta_k/k|$ is …

Hypothesis: Lemma.erdos_317.variants.claim2 (eventually, every nonzero $|\sum _{k\le n}{\delta }_k/k|$ is $>1/\mathrm{lcm}(1..n)$) reduces to a local statement. Equality can only happen when $\sum {\delta }_{k}L/k=\pm 1$, and that is impossible whenever some prime $p\in (n/2,n]$ has $L/p\not\equiv \pm 1(\mathrm{mod}p)$, because only $k=p$ contributes mod $p$. Computation confirms the obstruction exists for every $5\le n\le 3000$, and no equality occurs for $5\le n\le 26$ (exhaustive search). Making this rigorous for all large $n$ would settle claim2, and the reduction alone is a useful verified lemma. Method: (1) In Lean, prove the reduction lemma: the sum times $L$ is an integer, so a nonzero sum has $|\text{sum}|\ge 1/L$, with equality only if the integer numerator is $\pm 1$. Prove the mod-$p$ lemma: for prime $p\in (n/2,n]$, numerator $\equiv {\delta }_p\cdot (L/p)(\mathrm{mod}p)$. (2) Look for an argument that some $p\in (n/2,n]$ always has $L/p\not\equiv \pm 1$, for example by pairing two primes $p<q$ in $(n/2,n]$ and using $L/p\cdot p=L/q\cdot q$ to derive a contradiction when both residues are $\pm 1$. Also try the primes in $(n/3,n/2]$, where the residue lies in $(L/2p)\cdot \{0,\pm 1,\pm 2,\pm 3\}$. (3) If no all-$n$ argument closes, submit the verified reduction lemmas as notes only. Check everything with check_candidate. Threshold: 0 (must reach) Estimated cost: 60 min Why it's new: No notebook entry touches 317 (I searched; the related entries are N3, N4, N5, N12, N18 and N20, which cover 1065 and 1068 only). The mod-$p$ obstruction and the search up to $n=3000$ are new data from this unit, posted to chat. Related: N3, N4, N5, N12, N18, N20