Erdős Problem 336: why the constant is one third

The problem and why it is difficult

For each r ≥ 2, let h(r) be the largest exact order of an asymptotic basis of variable order at most r. The problem asks for the limit of h(r)/r².

The difficulty is not the lower bound: explicit periodic bases already suggest the quadratic scale and the coefficient 1/3. The hard direction is a uniform upper bound for every asymptotic basis. Three layers interact:

• the original set is infinite and only represents sufficiently large integers;
• after normalization, the relevant obstruction lives in finite cyclic groups;
• the sharp coefficient depends on rank-one geometry, so a coarse small-doubling theorem loses too much.

Even after reducing to a finite cyclic problem, one must show that a primitive set with short variable-length representations has a short common exact representation length. The extremal configurations resemble thin progressions, and every error of one fibre can change the sharp 1/3 coefficient.

Where the natural approaches stalled

A first route was to import a general inverse theorem for small-doubling sets. That was both much heavier than necessary and insufficiently sharp at the endpoint. A more specialized moderate-torsion route was sharper, but formalization exposed two genuine obstructions in the natural argument.

First, a printed unique-difference estimate loses a factor of two. The claimed bound is contradicted by

A = {0,1,3} ⊂ Z/6Z,

which has four uniquely represented ordered differences although |A|²/4 = 9/4. The prose argument counts undirected Mantel edges as if they were ordered differences. The high-power setting repairs this through Ruzsa’s triangle inequality, but the printed lemma cannot simply be imported.

Second, the endpoint representation-selection argument omits a critical three-point case. For

C = {0,x,2x},

the two new sums are 3x and 4x. Their unavoidable endpoint loads are 1 and 3, not the balanced bound 2 needed by the generic counting argument. Reorienting the progression does not fix this. Pure deficiency arithmetic remains short by exactly one far-fibre term, and treating the progression quotient as an immediate rank-one certificate is unsafe because its lift can retain two independent directions.

These failures identified the real bottleneck: the proof needed exact endpoint geometry, not a broader inverse theorem.

The route that worked

The proof first transfers the infinite problem to a finite cyclic removal statement. A dyadic high-power argument finds a scale with doubling below 9/4. Dense alternatives, bounded quotient alternatives, and rank-one alternatives are then handled separately. The rank-one endgame is encoded by an exact two-generator lattice diagram; its L-shape area inequality gives

3|G| ≤ (H+2)²,

which is the geometric source of the coefficient 1/3.

The central structural step rectifies a cyclic set into a graph

T ⊂ ℤ × ZMod N

supported between two occupied integer fibres, 0 and l. Quotienting by the displacement between these endpoints produces a finite endpoint quotient B. Let F be the Kneser stabilizer of B+B, let C=B/F, and let

D = (C+C) \ C

be the genuinely new sum classes.

The proof then exhausts the endpoint possibilities:

• |D|=0 gives the desired progression-plus-subgroup certificate directly;
• |D|=1 is excluded by a sharp two-piece projection inequality;
• |D|≥3 in the nonvertical branch is excluded by representation selection or a two-class/three-sum-class quotient;
• a vertical stabilizer forces the double-set saturation defect to be no larger than the original-set defect, contradicting full primitivity;
• the remaining |D|=2 nonvertical case is resolved by a complete classification of three-point critical sumsets.

That final classification was the decisive local breakthrough. Every three-point set with five double sums has one of three forms:

1. a load-two selector exists;
2. a subgroup quotient has two classes for the set and three for its double;
3. the set is the genuine progression {0,x,2x}.

The first two forms are ruled out by the existing sharp inequalities. In the progression form, direct integer-projection fibre geometry supplies the missing information that deficiency counting could not see, and excludes the branch.

From normalized endpoints back to the original set

The endpoint theorem initially applies only to a normalized rectified graph. Four exact transport results connect it to the original cyclic set:

• translation preserves cardinality, doubling, affine generation, and subgroup-saturation defects;
• strict-half rectification preserves |A|, |A+A|, and the number of quotient fibres;
• lifted progression certificates descend to cyclic rank certificates;
• the homomorphism

θ(i,x) = π(x) - i

vanishes on the rectified graph. Consequently, the vertical preimage of the endpoint stabilizer lies inside the rectifying kernel π.ker.

This last observation permits relative vertical primitivity instead of an unjustified absolute assumption. The normalized endpoint assembly therefore proves the fully primitive rectifiable theorem. Balanced and small-defect subgroup quotients then descend by strong induction, yielding the full rectifiable 3n-3 theorem. The finite high-power reduction and infinite transference complete the upper bound, while the periodic construction supplies the matching lower bound.

A final statement audit also closed a logical loophole: merely proving convergence for every extremal function could be vacuous if no such function existed. Eventual cyclic bounds can be padded with retained zeros to cover every smaller parent length; they therefore bound every admissible exact order. Since exact order one is always attainable, Nat.findGreatest selects an attained finite maximum for each r≥2. The final theorem explicitly proves both existence and convergence.

Verification

The result is formalized in Lean 4.31.0 with Mathlib revision fabf563a7c95a166b8d7b6efca11c8b4dc9d911f.

The executable checker:

1. validates a SHA-256 manifest of all 191 research source files;
2. builds the complete final dependency graph (8729 build jobs);
3. checks an independently duplicated, nonvacuous statement of the problem;
4. rejects sorry, admit, and project-declared axioms throughout the research tree;
5. runs #print axioms on the final theorem.

The only reported dependencies are Lean’s standard propext, Classical.choice, and Quot.sound. The checker ends with:

PASS: Erdős Problem 336 has verified value 1/3.

Thus the limit is exactly

1/3.