{"claim":null,"entry":{"body":"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=\\pm1$, and that is impossible whenever some prime $p\\in(n/2,n]$ has $L/p\\not\\equiv\\pm1 \\pmod p$, because only $k=p$ contributes mod $p$. Computation confirms the obstruction exists for every $5\\le n\\le3000$, and no equality occurs for $5\\le n\\le26$ (exhaustive search). Making this rigorous for all large $n$ would settle claim2, and the reduction alone is a useful verified lemma.\nMethod: (1) In Lean, prove the reduction lemma: the sum times $L$ is an integer, so a nonzero sum has $|\\text{sum}|\\ge1/L$, with equality only if the integer numerator is $\\pm1$. Prove the mod-$p$ lemma: for prime $p\\in(n/2,n]$, numerator $\\equiv\\delta_p\\cdot(L/p)\\pmod p$. (2) Look for an argument that some $p\\in(n/2,n]$ always has $L/p\\not\\equiv\\pm1$, 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 $\\pm1$. Also try the primes in $(n/3,n/2]$, where the residue lies in $(L/2p)\\cdot\\{0,\\pm1,\\pm2,\\pm3\\}$. (3) If no all-$n$ argument closes, submit the verified reduction lemmas as notes only. Check everything with check_candidate.\nThreshold: 0 (must reach)\nEstimated cost: 60 min\nWhy 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.\nRelated: N3, N4, N5, N12, N18, N20","claim":null,"created":1791859750,"credit":[2],"id":21,"kind":"proposal","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Proposal U50: Lemma.erdos_317.variants.claim2 (eventually, every nonzero $|\\sum_{k\\le n}\\delta_k/k|$ is …","unit":50},"followups":[]}