claimroutine

Outer computation uses O(B) space total

Whole outer computation uses O(B)O(B) bits, with digit queries always halting
space accounting making it a logspace transducer
Claim·§12.2 A dyadic approximation at the specified start·inside thmDeterministic logspace approximation of acceptance probability

Statement (paper)

The whole outer computation, including the master environment, current cursor, catalyst, shared scratch, suspended controller records, and the fixed number of additional registers (top parameters and designated start, environment enumeration index, EE, hh, current count, binary-search endpoints and candidate, digit index, signed numerator accumulator), uses only O(B)O(B) bits of memory, counted once for the whole computation and not once per recursive level. Moreover every digit query terminates on every environment, including the inaccurate ones, and the output is written only after the median is computed.

In plain English

The entire outer computation, with its master environment, cursor, catalyst, scratch, suspended controller records and a fixed number of extra registers, uses only O(B)O(B) bits in total, counted once rather than per recursive level. Every digit query also halts on every environment, even inaccurate ones, and output is written only after the median is computed.

Why it's here

This does the space accounting for the fixed-precision theorem: the controller interfaces from the controller realization theorem hold for every master environment and cost O(B)O(B) space, so the outer registers add only O(B)O(B) more. Because digit queries always halt and nothing is output before the median is known, the procedure is a genuine logspace transducer, which the polynomial-time counting claim then builds on.
Classified routine:
Direct space bookkeeping: the controller-realization theorem already gives O(B)-space restoring interfaces, and adding a constant number of O(B)-bit outer registers, plus the standard composition argument for logspace transducers (output written only at the end), gives the bound.

Uses

thmController interfaces have restoring O(B)-space implementations

Used by

claimTransducer runs in polynomial time

Sources

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

Phase 2 aligns this node to a Lean declaration.