claimroutineinferred_dep

Padding preserves acceptance probability exactly

Padding makes

U

y_x

accept with exactly

M(x)

's probability

links the library's answer to the language of

M

Claim·§13.3 Padding and exact preservation of acceptance probability·inside thmEffective compiler from randomized to deterministic logspace

Statement (paper)

Under the stated hypotheses on

M

(halting within

(n+2)^a

steps, using at most

b\lceil\log(n+2)\rceil

work bits), all eligibility checks pass for the padded input

y_x

of length

N_{\mathrm{pad}}=2^{PB_n}

, no resource cutoff changes a promised source run, and hence

\Pr[U(y_x)\text{ accepts}]=\Pr[M(x)\text{ accepts}]

exactly, with no conditioning or additional approximation. In particular the decision of

A(y_x)

is the decision required for

L_M

In plain English

M

halts within

(n+2)^a

steps and uses at most

b\lceil\log(n+2)\rceil

work bits, then on the padded input

y_x

of length

2^{PB_n}

the interpreter

U

passes all its eligibility checks and never cuts off a run. Hence

\Pr[U(y_x)\text{ accepts}]=\Pr[M(x)\text{ accepts}]

exactly, so the decision of

A(y_x)

is the decision needed for

L_M

Why it's here

The padded length is chosen so that the interpreter's step and work-tape limits from the compiler-interpreter lemma are at least

M

's promised bounds. Every run of

M

is then simulated faithfully with no truncation, and the two acceptance probabilities agree exactly, with no conditioning or approximation. This lets the later steps apply the library algorithm

A

y_x

and read off the answer for

M

x

Classified routine:

Standard padding argument: the padded length is chosen so that the fixed interpreter's resource limits from lem-compiler-interpreter exceed M's promised bounds. Faithful, untruncated simulation then follows by direct bookkeeping, as in classical universal-machine and padding arguments.

Uses

lemFixed interpreter with enforced resource bounds

Used by

claimCallback compiles virtual padded input reads

Sources

PaperOpen

Section: §13.3 Padding and exact preservation of acceptance probability
Page: —
Label: —
Line: sections/compiler.tex:256

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Padding preserves acceptance probability exactly" rests on lem:compiler-interpreter