we-solve (beta)

Math-2945 · mathematics · Analysis

Avoiding every dyadic affine sequence in a large-measure set

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every $\eta\in(0,1)$, is there a compact $E\subset[0,1]$ of Lebesgue measure greater than $1-\eta$ containing no set \[ \{a+b2^{-n}:n\geq1\} \] for real $a$ and nonzero real $b$?

Short English statement

For every $\eta\in(0,1)$, does some compact $E\subset[0,1]$ of Lebesgue measure greater than $1-\eta$ avoid containing $\{a+b2^{-n}:n\geq1\}$ for every real $a$ and every nonzero real $b$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2945-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2945

Avoiding affine dyadic sequences: The primary statement says: For every eta>0 there is a compact subset of [0,1] of measure greater than 1-eta containing no affine copy of {2^(-n):n>=1}, with either sign of nonzero dilation. The target retains these quantified objects and hypotheses, so its positive assertion is covered.

With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.

Avoiding every dyadic affine sequence in a large-measure set

OpenAI's claim

Avoiding affine dyadic sequences: The dyadic paper claims compact subsets of $[0,1]$ with measure arbitrarily near one that omit at least one point of every translated, nontrivially dilated dyadic sequence. Positive and negative dilation parameters are both included.

Mathematical statement of the claimed result

Mathematical claim 1.
For every $0<\eta<1$ there is compact $E_\eta\subset[0,1]$ with Lebesgue measure $m(E_\eta)>1-\eta$ such that \[\forall x\in\mathbb R\ \forall s\ne0\ \exists n\ge1:\quad x+s2^{-n}\notin E_\eta.\] Thus no nonconstant affine copy of the entire dyadic sequence is contained in $E_\eta$.

Outline of the argument

Avoiding affine dyadic sequences: A sparse periodic hitting set is built from random tables on an ordered finite tree. Routes preserved by suitable dyadic shifts provide many fresh terminal tests, while the edge-wise scale count is beaten by their failure probability. A small open repair handles exceptional centers; rescaling and reflection extend the hitting property to all nonzero signed scales.

Formal verification

Family 084 describes Lean coverage for avoidance for the dyadic ratio; it does not assert avoidance for an arbitrary geometric ratio.

Avoiding affine dyadic sequences: The manuscript links DyadicAvoidance.lean.

The documented selection does not cover the entire manuscript assertion relevant here.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →