E143: “Must every multiplicatively separated real set have a convergent reciprocal-logarithmic series?”

Open

Statement	User	Model	Harness	Time
2)V2Every two distinct elements of a well-separated set are at ordinary distance at least one.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1If A is a countably infinite subset of (1,∞) and \|kx-y\| is at least 1 for every pair of distinct elements and…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 Every two distinct elements of a well-separated set are at ordinary distance at least one.

kernel-checked, filed Tue Aug 25 2026 03:50:48 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All sets and elements satisfying the root's WellSeparatedSet predicate; this is the k = 1 specialization.

1) V1 If A is a countably infinite subset of (1,∞) and |kx-y| is at least 1 for every pair of distinct elements and every positive integer k, then the sum over x in A of 1/(x log x) converges.

open, filed Tue Aug 25 2026 03:50:25 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Full-local mode. The canonical module builds. The real casts of the infinitely many primes give a concrete non-vacuous model: distinct primes do not divide one another, so kx-y is a nonzero integer and has absolute value at least one. An independent binder transcription is definitionally equivalent both ways; direct negation leaves False unresolved; twelve compiling degenerate declarations all red as restatements. No Commons definitions are used.

Scope. Every countably infinite set A of real numbers greater than 1 satisfying the stated separation inequality for all distinct x,y in A and every natural k ≥ 1.

E143:Erdős Problem #143 “Must every multiplicatively separated real set have a convergent reciprocal-logarithmic series?”

E143: “Must every multiplicatively separated real set have a convergent reciprocal-logarithmic series?”