claimroutine

Parameter orders and balance inequalities

Claim·§4.7 Choosing the parameters·inside lemExplicit parameter choice satisfies layout hypotheses

Statement (paper)

For all sufficiently large

n

, the parameters satisfy

r=\Theta(\sqrt\lambda/\nu^2)

Q=\Theta(\lambda/\nu)

and

R=\Theta_\beta(\sqrt\lambda)

; in particular

r\ge2

R\ge32

and

6R\le Q

. Moreover

D\le2^{\lambda/128}

, and the two balance inequalities

2(b+w)D^2\le n\le M

and

2Qr^2\le n

hold.

In plain English

For large

n

, the parameters have sizes

r=\Theta(\sqrt\lambda/\nu^2)

Q=\Theta(\lambda/\nu)

and

R=\Theta_\beta(\sqrt\lambda)

, so

r\ge2

R\ge32

and

6R\le Q

. Also

D\le2^{\lambda/128}

, and both

2(b+w)D^2\le n\le M

and

2Qr^2\le n

hold.

Why it's here

This claim fixes the asymptotic sizes of

r

Q

R

and checks the size constraints that the layout lemma needs, so later claims can use these orders directly. The balance inequalities hold because

D=r^{2Q}

is at most

2^{\lambda/128}

while

b,w\le\lambda^\beta

are only polylogarithmic in

n

. The later claims on the binomial tail and the cost terms build on these bounds.

Classified routine:

Direct asymptotic bookkeeping from the explicit parameter definitions: it checks that

D=r^{2Q}\le2^{\lambda/128}

and that the polylogarithmic

b,w

satisfy the balance inequalities. No new idea is needed beyond substituting the definitions and comparing growth rates.

Uses

Nothing else in the paper

Used by

claimInterpolation interval captures binomial massclaimThree cost terms are balancedclaimParameters computable and checkable in polylog time

Sources

PaperOpen

Section: §4.7 Choosing the parameters
Page: —
Label: —
Line: main_full_version.tex:2777

Leannot aligned

Phase 2 aligns this node to a Lean declaration.