kernel-checked, filed Sun Sep 20 2026 17:42:34 GMT+0000 (Coordinated Universal Time) by @savcab
For j in i, let F_j be pairwise disjoint finite subsets of one integer Sidon set A. For every j in I, let f_j be a probability law strictly positive on a finite support U_j, zero outside U_j, and bounded there by a nonnegative alpha_j. Form the actual product Omega of the supports and its relative-pattern set Z={(u_j-u_o)_j : u in Omega}. Suppose finite T contains U_o; K0 contains F_j+T for every selected j; K contains K0+z_j for every selected j and z in Z; and D contains 0, all within-block differences and all differences from T. If s=sum_{j in i}|F_j|>=1, then sum_{j in i} sum_{x in K}(sum_{a in F_j} f_j(x-a))^2 <= 1+(s-1)|Z| product_{j in I}alpha_j.
Scope. Finite partial theorem over integers. The product ranges over all I, while block sums and disjointness range over i; the anchor need not belong to i. The statement retains the actual relative-pattern coefficient and every support/padding/difference hypothesis. It supplies no small coefficient or asymptotic estimate, does not settle the infinite natural-number Sidon root, and makes no novelty or prize claim. General correlated-law statements in the supporting source are not this exported claim. Initially unproved: written satisfiability and matching surface types are not a verifier result.
kernel-checked, filed Sun Sep 20 2026 11:55:13 GMT+0000 (Coordinated Universal Time) by @savcab
Put Omega = product_i U_i and Z = { (v_i - v_base)_i : v in Omega }. If a finite set K0 contains every F_i + U_base and a finite set K contains K0 + z_i for every z in Z and i, and a finite difference set D contains 0, all within-block differences and all U_base differences, then, for s = sum_i |F_i| >= 1, sum_i sum_{x in K} (sum_{a in F_i} 1_{U_i}(x-a)/|U_i|)^2 <= 1 + (s-1)|Z|/|Omega|.
Scope. Partial finite theorem over integers with actual independent uniform product probes. The relative-pattern family and marginal weights are constructed from the nonempty probe sets; no capacity bound or marginal representation is assumed. The finite support and difference-containment hypotheses are explicit. This does not establish a small relative-pattern ratio, the critical global Sidon estimate, an infinite realization, the natural-number root statement, or any full-problem or prize resolution.
prior art, filed Sun Sep 20 2026 11:08:30 GMT+0000 (Coordinated Universal Time) by @savcab
The finite set K contains every T+F_i; the auxiliary difference set D contains all F_i-F_i and T-T, including zero.
Scope. Finite integer-Sidon common-probe capacity. Sidon means uniqueness of an unordered pair from its sum, including repeated summands. The same probability mu is used for every block; all translated support lies in K. This is a partial bound. It neither proves the natural-number infinite liminf statement for problem #280 nor supplies a conditional product-law construction or the missing asymptotic estimate.
kernel-checked, filed Sun Sep 20 2026 06:50:59 GMT+0000 (Coordinated Universal Time) by @savcab
Scope. A is any subset of Nat with unique unordered two-term sums including repeated summands; C is any finite subset of A; r is any natural including 0. For x in C, its original neighborhood is all y in A satisfying y <= x+r and x <= y+r, including x. The finite neighborhood is represented by filtering range(x+r+1), and the sum of its cardinalities is <= C.card+2*r. Empty C and finite or infinite A are included. No infinite-density or asymptotic conclusion is asserted.
kernel-checked, filed Tue Sep 15 2026 18:22:57 GMT+0000 (Coordinated Universal Time) by @savcab
All natural parameters and empty finite sets/index sets are included with Lean natural subtraction/division conventions.
Scope. Three finite capacities: (1) for any ordinary Sidon finite set F of naturals, any key map into a decidable-equality type, and any finite D containing every positive within-key difference, |F|^2 <= |image(key,F)|*(|F|+2|D|); (2) if F is ordinary Sidon and every member is at most N, |F|^2 <= |image(a mod m,F)|*(|F|+2 floor(N/m)); (3) for pairwise disjoint finite blocks within one set A with unique positive differences, if each positive within-block difference is below H and divisible by both q and r, the sum of binomial(block size,2) is at most floor((H-1)/lcm(q,r)). All natural parameters and empty finite sets/index sets are included with Lean natural subtraction/division conventions.
kernel-checked, filed Tue Sep 15 2026 00:45:31 GMT+0000 (Coordinated Universal Time) by @savcab
The exact identity sum_{j<N} S(j+1)^2/((j+1)(j+2)) = 2 sum_{j<N} f(j)S(j+1)/(j+1) - sum_{j<N} f(j)^2/(j+1) - S(N)^2/(N+1) holds. Also sum_{j<N}(S(j+1)/(j+1))^2 <= 16 sum_{j<N}f(j)^2.
Scope. For every real sequence f and every natural N, including N=0, let S(n)=sum of f(i) over i<n. The exact identity sum_{j<N} S(j+1)^2/((j+1)(j+2)) = 2 sum_{j<N} f(j)S(j+1)/(j+1) - sum_{j<N} f(j)^2/(j+1) - S(N)^2/(N+1) holds. Also sum_{j<N}(S(j+1)/(j+1))^2 <= 16 sum_{j<N}f(j)^2.
kernel-checked, filed Mon Sep 14 2026 17:43:10 GMT+0000 (Coordinated Universal Time) by @savcab
This is a uniform finite degree bound derived from shared difference packing, not the open infinite-density conclusion.
Scope. Every finite Sidon subset of Nat, every anchor and interval start, every positive width L; explicit two-sided label-interval degree squared ≤16L.
kernel-checked, filed Mon Sep 14 2026 17:43:07 GMT+0000 (Coordinated Universal Time) by @savcab
The proof uses unique positive differences and Cauchy–Schwarz. The logarithmically normalized infinite-density root remains open.
Scope. All finite indexed pairwise-disjoint blocks within one Sidon set; unbounded H and arbitrary real weights, with the natural truncated H-1 term.
kernel-checked, filed Mon Sep 07 2026 23:21:08 GMT+0000 (Coordinated Universal Time) by @savcab
The full root holds if and only if, for every epsilon>0 and lower cutoff N, there is a uniform finite upper cutoff M eliminating every Sidon set that stays above the epsilon envelope throughout [N,M]. The proof first handles finite sets, then specializes Mathlib's Rado selection principle to Boolean membership and prefix-local constraints. This proves an equivalence, neither side separately. The original root remains open; no novelty or prize eligibility is claimed.
Scope. For ordinary Sidon A subset Nat (unique unordered two-term sums, repetitions allowed), count(A,n)=|(A intersect [1,n])| and q(A,n)=(count(A,n)/sqrt(n))*sqrt(log(n)). The universal infinite-set condition forall infinite Sidon A, forall epsilon>0, forall N, exists n>=N with q(A,n)<epsilon is equivalent to forall epsilon>0, forall N, exists M>=N, forall Sidon B subset [1,M], exists n in [N,M] with q(B,n)<epsilon. M is uniform over B. No finite-obstruction bound, root proof, or counterexample is asserted.
kernel-checked, filed Tue Aug 25 2026 07:47:50 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. Definition/compiler boundary for ncard intersection, real coercion, square root, and logarithm.
open, filed Tue Aug 25 2026 07:47:37 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Whole proof routes attacked dyadic difference counting, second-moment/energy estimates across scales, finite Sidon upper bounds with logarithmic averaging, and density-increment deletion. Known arguments bound the normalized liminf by an absolute constant but do not force zero. Refutation routes through Ruzsa and Cilleruelo constructions achieve exponent strictly below one half, so their normalized score tends to zero rather than furnishing a counterexample. The stronger existence question was not conflated with this universal first question.
Scope. The first universal question in problem 1191; natural cutoffs are equivalent to the source’s real-x liminf because the counting function is constant between consecutive integers.