claimroutineinferred_dep

Transducer runs in polynomial time

Transducer runs in time

2^{O(B)}=(n+2)^{O(1)}

running-time part of the fixed-precision theorem

Claim·§12.2 A dyadic approximation at the specified start·inside thmDeterministic logspace approximation of acceptance probability

Statement (paper)

Each digit query is a halting deterministic computation with

O(B)

work bits, so on its fixed input it has at most

2^{O(B)}

complete configurations and hence runs for at most

2^{O(B)}

steps. Since there are

2^{O(B)}

environment encodings,

O(K+1)

binary-search passes, and

K+1

digit queries per numerator, the total running time of the transducer is

2^{O(B)}=(n+2)^{O(1)}

In plain English

The deterministic transducer that outputs the dyadic approximation runs in time

2^{O(B)}

, which is polynomial in

n+2

, because each digit query halts within

2^{O(B)}

steps and only

2^{O(B)}

queries are made overall.

Why it's here

This is the running-time part of the parent theorem. It counts configurations to bound each digit query by

2^{O(B)}

steps, then multiplies by the number of environment encodings, binary-search passes and digit queries. With

B=O(\log(n+2))

the product is

(n+2)^{O(1)}

, complementing the logarithmic space accounting of the previous claim.

Classified routine:

Standard configuration-counting argument: a halting deterministic machine using O(log n) space runs in polynomial time (it cannot repeat a configuration). Here it is combined with a direct multiplication of the numbers of environment encodings, binary-search passes and digit queries.

Uses

claimOuter computation uses O(B) space total

Used by

Nothing in the paper

Sources

PaperOpen

Section: §12.2 A dyadic approximation at the specified start
Page: —
Label: —
Line: sections/conclusion.tex:264

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Polynomial time by configuration counting" rests on claim-thm-fixed-precision-6