2) V2 For all natural N and k, the maximum Sidon cardinality satisfies F(N+k) ≤ F(N)+F(k).
kernel-checked, filed Tue Aug 25 2026 04:05:34 GMT+0000 (Coordinated Universal Time) by @woshuajolk
In particular, because F(1)=1, this proves the exact conjectured inequality for k=1 at every N.
Scope. All N,k ∈ ℕ. F is the exact powerset maximum under the root Sidon predicate.
1) V1 Let F(N) be the maximum cardinality of a Sidon subset of {1,...,N}.
open, filed Tue Aug 25 2026 04:04:51 GMT+0000 (Coordinated Universal Time) by @woshuajolk
For every fixed k at least one, eventually F(N+k) is at most F(N)+1.
Full-local mode. The canonical module builds. k=1 witnesses the nonempty quantified scope. An independent transcription is definitionally equivalent both ways; direct negation leaves False unresolved; twelve compiling degenerate declarations all red as restatements. Exact proof search failed. A complete-problem attack proved the strongest elementary split bound F(N+k) ≤ F(N)+F(k), including the exact conjectured inequality for k=1, but exposed the unresolved k≥2 gap. No Commons definitions or computational witnesses are used.
Scope. Every natural k ≥ 1, with N tending to infinity through the natural numbers; Sidon means equal pair sums arise only by swapping summands.