Manuscript Oai279-A@1 · Oai279-A.tex · lemma · a1abc73f

Lemma: The padding needed for p *>1/2

Stage 1: audit the five interfaces without importing them › Interface 4: completion, deferred filters, and exact output · lines 556–591 · proof included or linked

Oai279-A@1#lem:pstar

Back to manuscript

With the source convention $n \geq 128$ and $L = n^{10}$ ,

1 - 2^{- 58} \leq 1 - n^{10} 2^{- n} \leq p_{*} < 1.

In particular $p_{*} > 1/2$ . It is a dyadic rational with denominator exponent at most $n^{11}$ .

Proof. Bernoulli's inequality gives

(1 - 2^{- n})^{n^{10}} \geq 1 - n^{10} 2^{- n} .

The sequence $a_{n} = n^{10} 2^{- n}$ decreases for $n \geq 128$ :

\frac{a _{n + 1}}{a _{n}} = \frac{( 1 + 1/ n ) ^{10}}{2} \leq \frac{1}{2 ( 1 - 10/ n )} < 1.

Here the middle inequality follows by bounding the finite binomial sum by the geometric series with ratio $10/ n < 1$ . At $n = 128$ ,

a_{128} = 2^{70 - 128} = 2^{- 58} .

The strict upper bound $p_{*} < 1$ is immediate. Finally,

p_{*} = \frac{( 2 ^{n} - 1 ) ^{n^{10}}}{2 ^{n^{11}}},

which proves the denominator bound.

Displayed formulas in this passage

unlabeled · line 559
$1 - 2^{- 58} \leq 1 - n^{10} 2^{- n} \leq p_{*} < 1.$
unlabeled · line 568
$(1 - 2^{- n})^{n^{10}} \geq 1 - n^{10} 2^{- n} .$
unlabeled · line 572
$\frac{a _{n + 1}}{a _{n}} = \frac{( 1 + 1/ n ) ^{10}}{2} \leq \frac{1}{2 ( 1 - 10/ n )} < 1.$
unlabeled · line 582
$a_{128} = 2^{70 - 128} = 2^{- 58} .$
unlabeled · line 587
$p_{*} = \frac{( 2 ^{n} - 1 ) ^{n^{10}}}{2 ^{n^{11}}},$

Lemma: The padding needed for p *>1/2

Displayed formulas in this passage

Nearby in this section