Skip to content

CarryCompression.md

Latest commit

 

History

History
224 lines (166 loc) · 7.1 KB

CarryCompression.md

File metadata and controls

224 lines (166 loc) · 7.1 KB
Raw

Carry-Aware Compression for Erdos 530

Status

This note records a candidate improvement to the compression argument in Bailleul and Riblet's 2026 paper, On the largest Sidon subset in a finite subset of R^N. The finite combinatorial core, the shifted floor-map relation lemma, and the constant optimization are checked in CompressionRoute.lean. The two-parameter collision average below has a complete written argument but has not yet been formalized in Lean or independently peer reviewed.

If the remaining lemma survives review, the argument gives

H(n) >= (2 / (3 sqrt(3)) + o(1)) sqrt(n)
     = (0.3849001... + o(1)) sqrt(n),

improving the paper's constant 1 / (3 sqrt(3)) = 0.1924500... by a factor of 2. It does not prove the conjectural constant 1.

1. Keep both carry classes

Let A be an n-element subset of the integers and let m >= 3. For theta,tau in [0,1), write

u_(theta,tau)(a) = floor(m a theta + tau).

The paper keeps only points for which the fractional part of m a theta lies in one half of the circle. That makes u_theta mod m an exact Freiman 2-morphism, but it discards half the points in expectation.

The common phase tau cancels from both sides of every two-sum relation. Without the half-circle restriction, every additive relation therefore has only one unit of rounding error. If a + b = c + d, then

u_(theta,tau)(a) + u_(theta,tau)(b)
  - u_(theta,tau)(c) - u_(theta,tau)(d) in {-1, 0, 1}.

Indeed, this integer is the negative of the corresponding difference of two sums of fractional parts, which lies strictly between -2 and 2.

2. The full-circle collision bound

For fixed theta and distinct a,b in A, average the collision event over the common phase tau. If t denotes (a-b)theta mod 1, randomized rounding gives the triangular kernel

K_m(t) = sum over k in Z of max(0, 1 - |m(t-k)|).

Thus

Pr_tau[u_(theta,tau)(a) = u_(theta,tau)(b) mod m] = K_m(t).

Multiplication by the nonzero integer a-b preserves Haar measure on the circle. The periodic triangular kernel has area exactly 1/m, so averaging over both parameters gives

integral integral P_(theta,tau) dtau dtheta <= n(n-1)/(2m).

Choose one representative from every nonempty fiber of the resulting map. For fiber sizes r_i,

n - number_of_fibers
  = sum (r_i - 1)
  <= sum binom(r_i, 2)
  = P_(theta,tau).

Consequently, some pair (theta,tau) gives a subset C on which the map is injective and

|C| >= n - n(n-1)/(2m).

The common phase is important. Without it, the universal collision bound is 2/m and is sharp; averaging the phase lowers every pair to 1/m. The final retained main term improves the paper's n/2 - n^2/(2m) to n - n^2/(2m), at the price of the defects +1 and -1.

3. Parity kills the defects

Let

s = p^2 + p + 1,
m = 2s,

where p is a prime power. The integer s is odd. Instead of viewing the floor map in Z/mZ, use

phi_(theta,tau)(a) =
  (u_(theta,tau)(a) mod 2, u_(theta,tau)(a) mod s)

in Z/2Z x Z/sZ. Equality in this product is equivalent to equality modulo 2s, so the collision estimate is unchanged. The one-unit defect is

epsilon = (1 mod 2, 1 mod s),

whose first coordinate is nonzero.

Singer gives p+1 Sidon sets S_i covering Z/sZ. Lift them to

T_(r,i) = {r} x S_i,    r in Z/2Z.

These 2(p+1) sets cover the product. Each is Sidon, because equality of pair sums projects to equality inside S_i, while every first coordinate is the same. More importantly, if four points lie in one T_(r,i), the difference of their two pair sums has even first coordinate. It therefore cannot equal +epsilon or -epsilon. The only possible defect is zero, and the ordinary Sidon property finishes the pullback.

This product-cover argument is formalized by:

  • IsOneDefectMorphismOn;
  • sidon_preimage_of_one_defect;
  • parityProductPart_sidon;
  • parityProductCover;
  • one_defect_product_cover_extraction;
  • shiftedFloorParityMap_one_defect;
  • shiftedFloorParityMap_cover_extraction_from_image.

4. Constant calculation

Write m = (c + o(1))n, with c > 1/2. The retained set has size

(1 - 1/(2c) + o(1)) n,

and the parity-lifted Singer cover has

2(p+1) = (sqrt(2c) + o(1)) sqrt(n)

parts. The resulting coefficient is

f(c) = (c - 1/2) / (c sqrt(2c)).

It is maximized at c = 3/2, where

f(3/2) = 2 / (3 sqrt(3)).

Lean checks both the global bound and equality at c=3/2 in shifted_one_defect_compression_singer_constant_bound and shifted_one_defect_compression_singer_constant_at_three_halves. The Statistics MCP independently returned the numerical maximizer 1.5000000115 and value 0.38490017946.

Choosing s = (3/4 + o(1))n by the prime number theorem makes m = 2s = (3/2 + o(1))n, so this parameter choice is available asymptotically.

5. Gap audit

The following points have been checked explicitly.

  1. The floor error is an integer strictly between -2 and 2, hence is exactly -1, 0, or 1.
  2. For a fixed pair, common-phase averaging produces the triangular kernel above; its exact area over the circle is 1/m.
  3. Selecting one point per fiber does not remove any relation needed by the one-defect statement.
  4. s = p^2+p+1 is odd, so congruence modulo 2 and modulo s detects congruence modulo 2s.
  5. The lifted Singer family is a cover, not a partition; the averaging theorem only needs a cover.
  6. The parity argument works for repeated entries in Sidon's equation as well as for four distinct entries.

Still requiring external scrutiny or formalization:

  • formalize the two-parameter Haar-measure collision average, preferably first as a finite rational-grid argument and then by a limit;
  • connect the integer result to arbitrary finite subsets of R^N using the projection and Dirichlet-preservation lemmas from the paper;
  • obtain an independent mathematical review before treating the improved constant as established literature.

6. Why this is not yet the solution to Problem 530

The parity trick removes the forced half-circle loss, but two losses remain:

  • the pair-collision estimate deletes about n/(2c) points;
  • the parity lift uses about sqrt(2m) cover parts.

Optimizing those terms stops at 0.3849..., far below the conjectural constant 1. Reaching 1 still appears to require almost-lossless compression into a target of size (1+o(1))n, or a substantially stronger carry-robust Sidon cover. The separator/rigid-model and modulus-window program in experiments/README.md remains the longer-term route to that goal.

An exact CP-SAT side check searched for larger carry-robust sets, meaning sets whose distinct unordered pair sums are neither equal nor adjacent modulo m. For m = 14, 26, 42, 62, 114, the exact maximum sizes were 3, 4, 5, 6, 8, respectively, exactly matching the parity-lifted Singer sizes. At m = 146, the solver found size 9 but did not close its upper bound. This finite evidence gives no easy route to removing the parity-cover factor.