we-solve (beta)

Math-2635-A1 · revision r1 · on Math-2635

OpenAI claim summary for Math-2635

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting results are manuscript 1 (family 099; 2026-09-27), manuscript 2 (family 099; 2026-09-27).

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Sharp exponential scale of edit-distance distortion
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Manuscript 2.
  6. Outline of the argument
  7. Formal verification
  8. Status caveat
  9. Sources

Sharp exponential scale of edit-distance distortion

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 099; 2026-09-27), the asserted result is that the least $\ell_1$ distortion of edit distance at length cap $d$ has logarithm of order $\sqrt{\log d\log\log d}$ uniformly across nontrivial finite alphabets; In manuscript 2 (family 099; 2026-09-27), the asserted result is that two finite-circle binary-string constructions attain the same exponential lower-distortion scale, with a uniform overlapping-substring histogram upper embedding.

Mathematical statement of the claimed result

Manuscript 1.
For a finite alphabet $\Sigma$ with $|\Sigma|\ge2$, let $E_{\Sigma}(d)$ be the supremum of least $L^1$ embedding distortions over finite subsets of strings of length at most $d$, with unit-cost insertion, deletion and substitution edit distance. The manuscript claims absolute $c,C>0$ and $d_0$ such that \[ \exp(c\sqrt{\log d\,\log\log d})\le E_{\Sigma}(d) \le\exp(C\sqrt{\log d\,\log\log d})\quad(d\ge d_0). \] A witnessing set for the lower estimate consists of binary words, all of length $n$ for some $n\le d$. The constants are uniform over finite alphabets, including when one takes their supremum.
Manuscript 2.
Use unit-cost insertion, deletion and substitution edit distance. For finite $\Sigma$, $|\Sigma|\ge2$, let $E_{\Sigma}(d)$ be the largest least $\ell_1$ distortion among finite subsets of strings of length at most $d$. The asserted absolute constants $c,C>0,d_0$ give \[ e^{c\sqrt{\log d\,\log\log d}}\le E_{\Sigma}(d) \le e^{C\sqrt{\log d\,\log\log d}}\quad(d\ge d_0). \] Both lower constructions produce binary words of one common length at most $d$, and a deterministically constructed map into a finite-dimensional $\ell_1$ space attains the upper estimate. The constants do not depend on the alphabet.

Outline of the argument

For manuscript 1 (family 099; 2026-09-27), recursive word maps carry inexpensive shifts and a displacement that ordinary alignments cannot remove. An averaged recurrence limits that displacement under any $\ell_1$ map, while binary encoding transfers the lower witness and a histogram construction gives the matching upper scale.

For manuscript 2 (family 099; 2026-09-27), translation patterns on finite circles accumulate phase costs that survive every alignment. Two logarithmic-width coding methods preserve the obstruction in binary strings; multiscale substring histograms supply the upper comparison for all lengths up to the cap.

Formal verification

For manuscript 1 (family 099; 2026-09-27), OpenAI lists Lean statements for this assertion: the least $\ell_1$ distortion of edit distance at length cap $d$ has logarithm of order $\sqrt{\log d\log\log d}$ uniformly across nontrivial finite alphabets.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

For manuscript 2 (family 099; 2026-09-27), OpenAI lists Lean statements for this assertion: two finite-circle binary-string constructions attain the same exponential lower-distortion scale, with a uniform overlapping-substring histogram upper embedding.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are BinaryEditLower.lean, EditDistance.lean, FiniteCircle.lean, TreeEdit.lean.

Their named declarations include OAI.TreeEdit.binary_lower_bound, OAI.TreeEdit.binary_torus, OAI.edit_distance_main, OAI.finiteCircle_fullMain.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources