Exact derandomization of logarithmic space: L = RL = BPL

Proof. Let T(n) be a fixed polynomial upper bound on the running time. A vertex records a time in \{0,\ldots,T(n)\}, the finite control, all input and work head positions, and the contents of a sufficiently large box of O(\log(n+2)) work cells. Take elementary machine steps with fixed dyadic coin probabilities. A transition advances the time by one. Invalid configurations or moves leaving the box have no corresponding transition. The box is chosen large enough that this never affects a computation from the specified start.

Each elementary step has constantly many successor choices. To find predecessors, guess the old finite control, locally overwritten symbols, head movements, and coin choice, then check that the forward step gives the specified configuration. There are constantly many such guesses. Combine transitions with the same ordered pair of endpoints by adding their probabilities. Order the distinct successors and predecessors by their configuration encodings; their positions give paired ports for the resulting matrix entries. These lists have constant length, so duplicate removal, summed weights, and the inverse port are computed in logarithmic space by local enumeration. This base computation makes no recursive graph queries. All records use O(\log(n+2)) bits, and the read-only input can be consulted during these checks.

All input-head coordinates in the vertex universe are restricted to a fixed polynomial interval containing the positions reachable within T(n) local steps from their specified initial positions. Configurations and predecessor candidates outside that interval are invalid. To obtain a simulated head’s scanned symbol, compare its stored coordinate with the input boundaries, supply any required endmarker or off-data blank according to the source tape convention, and otherwise scan the real endmarked input to the designated position using a logarithmic-space counter. A position forbidden by the source tape convention remains invalid. The physical scan stays between the real endmarkers, even when a valid simulated coordinate is outside the data. This routine makes no recursive graph query.

An already halted computation keeps its complete tape and head data while its time advances. In particular, halted configurations are not merged into a single vertex. Let e be one precisely at accepting configurations at time T(n), and zero elsewhere. Final-time rows have no outgoing transitions. Thus S is strictly forward and substochastic, and it is nilpotent. Its inverse expression is the finite sum

Starting from any valid configuration, at most one reward can be collected, at final time. The sum is therefore a probability in [0,1]. At x_0 it is exactly the machine’s acceptance probability.□

Proof. The probability that an unrestricted H-by-r matrix is a frame is

For fixed positive-degree coefficients, a_0 is uniform, so any one evaluation is uniform in \mathbb F_P^H and independent of frame success. This proves the exact marginal retention probability. In the ranges used, take P2^{-k}\ge1. Then P2^{-k}\le L_k\le2P2^{-k}, proving comparability. The prime exponent can in fact make all these sides much larger than one.

Without conditioning on a frame, two evaluations at distinct field points are independent uniform vectors: the two evaluation functionals have rank two since h_0\ge2. Consequently

The first marginal after conditioning is still \pi_u, which proves the second assertion.

For the third assertion, in the unrestricted distribution the hit count has mean q\pi_a and variance at most q\pi_a, by pairwise independence. Chebyshev’s inequality bounds the stated lower-tail event by 4/(q\pi_a). Conditioning on frame success increases this probability by at most 1/q_{\rm fr}.

Finally, substituting \alpha y+\beta in a polynomial acts on its positive-degree coefficient columns by an invertible triangular matrix, with diagonal \alpha,\ldots,\alpha^{h_0-1}. It therefore preserves the frame condition. Its action on the full coefficient array is an invertible linear change of variables, so it preserves uniform measure conditional on that condition. Appending digits in radix D_0 has \alpha a power of D_0; taking P>D_0 ensures the required invertibility.□

Proof. Order the vertices compatibly with the strictly forward relation. For a fixed row x, the entry (E_*C)(x,y) involves only E_*(x,z) with z<y. Equation (4.4) therefore defines the row successively, in increasing column order. Columns at or before x receive zero. This proves existence and uniqueness in the stated class, without a contraction hypothesis. Monotonicity of the update map proves E_i\leq E_* and the nonnegativity of the differences.

Set T=C-E_*+E_*C. If a=(C+E_*C)(x,y), then Equation (4.2) implies

Thus T\geq0, and at every positive position of E_* one has T(x,y)\geq\theta_1f. Also

Consequently, for each fixed row x, its set A_x=\{y:E_*(x,y)>0\} has cardinality m_x\leq1/(\theta_1f).

Unroll the inequality E_*\leq C+E_*C along this row’s support. Each resulting term for E_*(x,y) is a product of entries of C along a sequence

Every substitution keeps the source coordinate equal to x: the recursive factor is E_*(x,z), while only its terminal coordinate changes. All intermediate vertices therefore belong to the same set A_x. Strict ordering makes a choice of intermediate vertices specify at most one such sequence. There are at most \binom{m_x}{j} such sequences, and each product is at most f^{j+1}. The expansion terminates because every sequence is strictly increasing. Therefore

Only the support of the single fixed row x was used here; the number of vertices in the whole graph does not enter the exponent.

Let \Delta_i=E_*-E_i. These matrices are nonnegative, and their row-x supports are contained in A_x. The Lipschitz bound gives

Outside A_x the left side is zero, so when this inequality is unrolled it suffices to use intermediate vertices from A_x at every step. After k steps there are at most \binom{m_x}{k} strictly increasing sequences of intermediate vertices. Their initial differences are at most fe^{1/\theta_1} by Equation (4.7), and their k transition factors are at most f^k. Thus

For k>m_x the first upper bound is zero. This proves Equation (4.5). The factorial eventually dominates the fixed exponential factor, giving the stated fixed choice of k_*.□

Proof. Equation (4.2) gives Q(0)=0 and 0\leq Q(t)\leq t for t\ge0. Consequently \widehat E_i\leq G_i. If \widehat E_{i-1}\mathbf 1\leq(i-1)\mathbf 1, then

For an individual entry,

This proves the pilot bounds by induction.

The sequence \widehat g_i is nonincreasing, so g\leq\widehat g_i for every i. Induction in Equations (4.10)–(4.14), using monotonicity of Q, proves E_i\leq\widehat E_i and G'_i\leq G_i. The map F\mapsto fQ((C+FC)/f)g, applied entrywise after forming the matrix product, is monotone. Its iteration from zero is therefore nondecreasing. The actual bounds follow from the pilot bounds.

A product of strictly forward matrices is strictly forward. A zero row of C remains a zero row in all these formulas, by induction from the zero correction. A zero column of C is a zero column of every product of the form FC and hence of every input and correction. This proves the remaining assertions.□

Proof. Fix i,y and condition on Y_f(y)=1. In a fixed row, the set \{w:G_i(x,w)>\eta_-f\} has cardinality at most k_*/(\eta_-f) by Lemma 4.2. Its expected number of retained members is at most D_{\rm row}: the specified terminal y, if in this set, contributes at most one, and Equation (4.8) applies to every other member. If the row gate is not full, at least K such members have been retained. Markov’s inequality therefore gives

Let A=\{x:G_i(x,y)\geq\delta_1f\} and n=|A|. Let N_A count its retained starts, and let L_A count those retained starts whose row gate is not full. Independence of the two channels and Equation (4.17) imply

Thus

The law of the start channel is unchanged by the conditioning, so Equation (4.9) gives

If n>R_*/f, Equation (4.16) ensures n\pi_f\geq\max(4J,40C_{\rm var}). Outside an event of probability at most 1/20, there are at least J retained high rows with full gates. Each has score exactly one, so the trial’s J-th largest score is one. All trial scores lie in [0,1], proving the first assertion. This argument used no independence among the row-gate failures.

For the second assertion let A_0=\{x:G_i(x,y)>\delta_0f\}, and let N_0 be its number of retained starts. A positive score must come from A_0. Pointwise the trial is at most \mathbf 1_{\{N_0\geq J\}}, and hence at most N_0/J. Its conditional expectation is at most |A_0|\pi_f/J\leq |A_0|C_\pi f/J. The asserted lower bound on |A_0| follows.

Finally, a positive \widehat g_i(y) implies U_i(y)<4/5, so the first assertion excludes a high-entry count greater than R_*/f. If g(y)>0, all pilot multipliers at y are positive. Apply the same bound to every G_i and then use G'_i\leq G_i from Lemma 4.2.□

Proof. Set A=G'_{k_*} and \delta=(E-E_{k_*-1})C\geq0. Then

Here and in the minimum the scalar \theta_1f denotes the constant entrywise bound. The second inequality follows from E\leq(A-\theta_1f)_+. It proves D\geq0. Since C\mathbf 1\leq\mathbf 1 and E\geq0,

Also D\leq C+EC, whose entries are at most f+f\sum_z E(x,z)\leq(k_*+1)f by Lemma 4.2. Strict forwardness and the support claims follow from the same formulas.

Because A(x,y)\leq k_*f, Equation (4.20) gives A-E\geq(\theta_1/k_*)A. On the other hand,

Since \theta_1/k_*<1, these two inequalities prove Equation (4.19). The remaining unsigned-term assertions are immediate from nonnegativity of the summands in the two input formulas.

For the good-column bound use the fixed point with this same multiplier g, and set \Delta=E_*-E. With T=C-E_*+E_*C,

If g(y)=1, the lower bound in Equation (4.2) gives T(x,y)\leq\theta_2f. Equation (4.5) gives \Delta(x,y)\leq q^{-1}f/32. This proves Equation (4.18).□

Proof. The row sum at x_i is r_i(x)\sum_yD(x,y)\leq1. Strict forwardness follows from that of D. Put t=D(x,y)/f. If t<\tau_1, then every routed entry is at most ft<f/q. If t\geq\tau_1, all fractions equal 1/D_0, so every entry is at most K_*f/D_0<f/q. This proves the density bound.

If a nonprimary fraction s_j(D(x,y)/f) is positive on a positive entry, then D(x,y)/f>\tau_0>\varepsilon_{\rm good}. Lemma 4.4 therefore implies g(y)<1. Since \gamma equals one through 1/2, this gives U^{\max}(y)>1/2, and hence r_j(y)=1. The primary factor is always one. Thus for every positive entry of D,

For a zero entry no identity of its fractions is needed. Multiplying Equation (4.23) by P^r and using Equation (4.27) proves Equation (4.26) entrywise.

It remains to count active vertices. Put

Every y\in\mathcal O has, for some pilot step i, more than J/(4C_\pi f) entries with G_i(x,y)>\delta_0f, by Lemma 4.3. Counting these incidences over all steps and all active rows, and using Lemma 4.2, gives

The assertion is also valid when n'=0, since then all matrices and detectors vanish. Thus

Every active child has an active parent, by the support conclusion of Lemma 4.4. A nonprimary child active as a row has r_i(x)>0, so its parent belongs to \mathcal O. A nonprimary child active as a column has a positive extra routing fraction and, as shown above, its parent has U^{\max}>1/2, so again belongs to \mathcal O. Therefore

where the last inequality is Equation (4.24).□

Proof. The assertion at l=0 is S=I-(I-S). The residual identity can be written as

Using Equation (4.26) and then the inductive hypothesis,

This proves Equation (4.29).

Every B_l is nonnegative. Every P_l^r has at most one nonzero entry per row, of value in [0,1], and thus P_l^c is substochastic. Apply Equation (4.29) to p_0, using (I-S)p_0=e. This gives the identity in Equation (4.30). Its lower bound follows from B_le\geq0; its upper bound follows from W_l\leq P_l^cp_0\leq1. Equation (4.31) is Equation (4.28) applied to e.

By Proposition 4.5, induction gives

There are at most |\mathcal A(C_l)| columns containing any positive entry, so each row sum of C_l is at most |V_0|2^lq^{-l}=|V_0|2^{-(H-1)l}. The all-primary projection has every row factor equal to one and hence (P_l^cp_0)(\bar x_l)=p_0(x). The identity in Equation (4.30), together with 0\leq P_l^cp_0\leq1, now proves Equation (4.32).

Choose an integer L such that (H-1)L>\log_2(16|V_0|). Since \log_2|V_0|=O(B), this is O(B). If p_0(x)=0, nonnegativity forces W_L(\bar x_L)=0. If p_0(x)\geq1/2, the strict error bound gives W_L(\bar x_L)>7/16. Finally,

because D_0 is fixed. Parent projection deletes one radix symbol, and appending a specified symbol is affine in the numerical ID. Thus these domain changes preserve the address convention required by the sampler and by the later implementation.□

Proof. The row gate can fail to be full only if at least K sampled columns have G(x,z)/a>r, where r=(1/2)/1000 is fixed. There are at most M_G/(ar) such deterministic columns. Conditional on Y_t(y)=1, the specified column contributes at most one hit and each other column has Y_a-hit probability at most C a, by Lemma 3.1. Thus the expected count is at most 1+CM_G/r. Conditioning also on the independent source channel does not alter this bound. Markov’s inequality makes the failure probability at most 1/8 by a sufficiently large K.

Where k_a(d_y)>0, we have h(d_y)=1. Therefore q_y=\mathbb E[R\mid Y_t(y)=1]\in[7/8,1] there, and the clipping does nothing. The conditional mean of Equation (5.11) is consequently k_a(d_y). Outside that support both sides vanish. If a row output is positive, its first entry exceeds 1/2 and its Kth first rank is below 1/1000. Hence there are at most K-1 positive entries. Boundedness follows from the clipped denominator. The routed fraction is deterministic at truth and obeys the same argument.□

Proof. Use F\mathbf 1\leq k_*\mathbf 1 from Lemma 4.2: (FA_b)\mathbf 1\leq F\mathbf 1, and (FA_b)(x,y)\leq c_b b\sum_zF(x,z). The last assertion follows by multiplying A_b\leq C on the left by the nonnegative matrix F.□

Proof. The row count argument in Lemma 5.1, with the correction thresholds, gives \Pr(R\ne1\mid\text{the two hits})\le1/8. If g_0(y)>0, every source with I(x',y)>0 belongs to the deterministic set in Equation (5.2). Conditional on X_u(x)=1, the number of sampled members of that set has expectation at most

The bound remains valid after conditioning on the independent terminal hit; it ignores the auxiliary row gate and therefore needs no additional independence between rows. If fewer than K_c such sources are sampled, the K_cth auxiliary rank is zero and T_y=1. Choose K_c\ge8(1+C R_*) to make \Pr(T_y\ne1\mid\text{the two hits})\le1/8. The union bound, without independence of the gates, gives \mathbb E[RT_y\mid\text{the two hits}]\ge3/4.

Since h(d_y)=1 on Q’s support, Equation (5.15) holds and c(q_y)=q_y there whenever g_0(y)>0. The claimed conditional identity follows by division by this exact conditional mean. If Q(d_y)=0 or g_0(y)=0, both sides of the identity are zero. In the latter case the pre-incoming quantity Q_{\rm at}(d_y)R/c(q_y) is still a well-defined bounded comparison target, even if the unclipped mean vanishes.□

Proof. For the main and preparatory products a nonzero entry has v>\vartheta/2 and \rho<\vartheta/500. There cannot be K such entries, since then the Kth rank would exceed \vartheta/2.

For an explicit class choose consistently computed approximations \widetilde v,\widetilde\rho with absolute errors at most \eta=\vartheta/10000, and set

Every positive main or preparatory entry belongs to A. An entry in A satisfies v_y>(3/8-1/10000)\vartheta>\vartheta/4 and \rho<(1/200+1/10000)\vartheta<\vartheta/100, so its witness I_{\vartheta} equals one. Its entry threshold exceeds its rank threshold, proving |A|\le K-1.

The support of I_{\vartheta} requires v>\vartheta/8 and \rho<\vartheta/50, again giving the same row bound. To access this score itself, the class

contains its support and has at most K-1 entries. A smooth unit witness on A_I is

The approximation margins imply A_I\subseteq\{J_{\vartheta}=1\}. Moreover 82/1000>3(27/1000), so this witness also has bounded row support and the required entry versus rank separation. The witness is an analytical output; its support need not be broadened recursively.

These arguments use the rank of the prescribed entire raw array. In particular, if at least K dummy positions have a common virtual default \beta, then \rho\ge\beta. A real position still equal to that default cannot meet either exposed class: the required lower bound on v=\beta exceeds the required upper bound on \rho. Thus omitted default positions do not create unlisted ports.□

Proof. The row and witness assertions are Lemma 5.5; clipping and multiplication by bounded factors do not enlarge supports. If a column has more than K_c entries in A, its auxiliary score is one at all those entries, so its K_cth auxiliary rank is one. Equation (5.12) makes T_y=0 there. Consequently every value deleted by Equation (5.18) was already zero. The surviving relation has the stated two degree bounds even when zero weights are retained. The argument applies to arbitrary raw arrays, so it applies equally to the estimated and true versions.

The cap removes every precursor port at an overfull column; it does not choose K_c of them. It is applied even when the particular entry has weight zero. Every surviving port still lies in A, so its pre-incoming witness I equals one regardless of a zero usage mask, incoming gate, or column multiplier. The broader auxiliary class A_I is used to enumerate scores for an incoming rank. It is not the capped correction relation used as a paired left factor in a product.

The classes are relations on row and column IDs, rather than multisets of paths. Choosing one port per relation element gives the stated combinatorial interface. Establishing its single-address enumeration and port pairing within the space bound is an implementation obligation; the degree argument does not itself grant random access to both IDs.□

Proof. All factors are bounded. On the union E of the two final nonzero supports, the triangle inequality for the products of sth roots gives

Outside E the left side is zero. The pre-incoming discrepancy may be charged on its entire row domain; it needs no incoming cap. Each column has at most 2K_c edges in E, by Lemma 5.6. By Equation (5.4), the root-Lipschitz incoming cutoff, and Equation (5.21),

Consequently its integrated contribution is at most

which is C\mathfrak d_{u,f}(I,I')^s.

The maximum over a fixed number of U_i values is Lipschitz, and the multiplier cutoff has Lipschitz root. Thus the last discrepancy is bounded in sth power by C\sum_i|U_i(y)-U_i'(y)|^s. Summing over E costs at most 2K_c/u per retained column. The vertex metric has weight 1/f instead, giving precisely the factor f/u in Equation (5.22). All columns in this comparison are in the common Y_f domain, including those whose final values carry a narrower usage mask. The common-tuple condition ensures that the vertex discrepancy at y is the same quantity for every old start. Explicitly, if m_E(y) counts the edges of E entering y, then for each i its contribution obeys

This is the column-counting step; it uses no independence between the two row tables and the vector estimates.

For a detector trial, Equation (5.4) bounds the trial discrepancy by the supremum of the input score discrepancies over retained starts. Its sth power is at most the sum of their sth powers. The factor Y_f(y)/f in the vertex metric is exactly the factor obtained by reversing the two sums in the row metric with u=a=f. Equation (5.21) gives Equation (5.23).□

Proof. Let \mathcal S consist of the elementary matrices with a single \pm1 off the diagonal, acting linearly, and the translations by \pm e_i, where e_i are the standard basis vectors of \mathbb Z^H. This is a fixed finite symmetric generating set of G_H. For a unitary representation \rho and a vector \xi, put

We first bound the distance from \xi to the invariant subspace.

For each coordinate pair \{i,j\}, embed the two-dimensional affine group on those coordinates, and let P_{ij} be the orthogonal projection onto the subspace fixed by its translations. This subspace and its orthogonal complement are invariant under that pair group, because its translation subgroup is normal. The eight generators in [33, Theorem 2.1, p. 152] belong to \mathcal S. Applying their relative Kazhdan constant 1/10 on the orthogonal complement gives

This is the projection argument in the proof of [33, Corollary 2.3, p. 154].

The projections P_{ij} commute: they are limits of averages of commuting coordinate translations. Their product P_{\rm tr} projects onto the subspace fixed by all translations. With q=\binom H2, telescoping the product gives

Since the full translation subgroup is normal, P_{\rm tr} commutes with every \rho(g). Its range carries a representation of G_H/\mathbb Z^H=\mathrm{SL}_H(\mathbb Z). Let P_{\rm inv} project onto the full G_H-invariant subspace, and let \kappa_H>0 be the Kazhdan constant for the elementary generators from [33, Theorem 2.6, p. 156]; adjoining inverse generators preserves the bound. Applying that constant on the range of P_{\rm tr} gives

Thus the same generating set controls distance to invariants in every unitary representation, with a constant depending only on H.

Now let \rho be the permutation representation of a finite transitive action, with the uniform probability measure, and put m=|\mathcal S|. The rational Markov operator

is self-adjoint, and its spectrum lies in [0,1]. The invariant functions are exactly the constants. For f orthogonal to constants, the preceding inequality and the Dirichlet identity give

This proves the uniform spectral gap.□

Proof. On a channel conditioned at y with side L, use coordinates (F,w), where F is its field frame and w=Av(y)\in\{0,\ldots,L-1\}^H. The constant column is uniquely determined by F,w,y. As observed above, F is uniform over frames and w is independent uniform in its box. Identify this box with (\mathbb Z/L\mathbb Z)^H. For (M,c)\in G_H act by

using reduction modulo P on the first coordinate and modulo L on the second.

This action is transitive. Reduction of \mathrm{SL}_H(\mathbb Z) contains the elementary generators of \mathrm{SL}_H(\mathbb F_P). That finite group acts transitively on ordered frames of length r<H: extend either frame to a basis and adjust a complementary column to make the change-of-basis determinant one. Once the frame has been moved, a translation adjusts w to any specified value. The two moduli need not agree. On an unconditioned channel use a public identifier and side P, giving the same description.

If the free bit length is Hq, identify its strings with (\mathbb Z/2^q\mathbb Z)^H and use the affine action on that coordinate alone. It is transitive. All currently free bit blocks can be concatenated into this one component; frozen bits are not transformed. There are a bounded number of components. Apply the lazy walk from Lemma 6.1 to a uniformly selected component. If there are J_{\rm comp} components and the single-component gap is at least \gamma_H, the product walk has gap at least \gamma_H/J_{\rm comp}. Here J_{\rm comp} is bounded independently of the field and bit lengths. The walk preserves the desired product measure.

Writing its gap as \gamma>0, we have \|K^d-\Pi\|_{2\to2}\le(1-\gamma)^d and \|K^d-\Pi\|_{\infty\to\infty}\le2. The diagonal case of the Riesz–Thorin interpolation theorem, already covered by Riesz [30, Theorems II and II', p. 472], gives

which has the required form. For Thorin’s complex extension, see [34, Introduction, §0.1; Russian translation, pp. 43–45].□

Proof. Consider a fixed affine generator (M,c) on a channel with retention side L. Enumerate the transformations

where e_1 selects the constant column and z ranges over a fixed finite box of integer vectors. That box contains all possible wraps: for w\in\{0,\ldots,L-1\}^H, every coordinate of Mw+c is bounded in absolute value by a fixed multiple of L plus a fixed constant. Since L\ge1 and the generators are fixed, one bound for z works for every side length.

Each transformation in Equation (6.1) is invertible. Left multiplication preserves the frame condition, and the added term changes only the constant column. It therefore preserves uniform measure on the full channel. It does not refer to the indicated identifier.

At that identifier, let w=Av(y) in its integer representatives. Check first that w is in the retention box, and then that Mw+c+Lz lies in the same box coordinatewise, using integer arithmetic before reduction modulo P. The unique valid wrap has coordinates z_i=-\lfloor(Mw+c)_i/L\rfloor. For this vector the evaluation of A' is the representative of the intended affine action modulo L. Applying these checks at every step gives the unique valid wrap sequence for a whole word.

The construction applies separately to the bounded number of channels. On a channel of side P the ordinary field reduction suffices; alternatively, the same wrap validation may be used at its public point. The free-bit torus has ordinary invertible affine operations and requires no unknown endpoint. Frozen bits remain fixed. Thus a word has only constantly many generator and wrap choices per step, giving the O(d)-bit description.

For each word and initial environment in the slice, exactly one variant survives. Its weight must be the weight of that word. In particular, the sum is not divided by the number of guessed wraps. This proves the asserted exact identity. All matrices have fixed dimensions and O(B)-bit entries; evaluating a bounded-degree polynomial or a word’s individual steps needs O(B) arithmetic scratch. A test depending on a vertex can be delayed until that vertex is current, with the required matrix state regenerated from the recorded transformations. Theorem 11.1 accounts for reversible restoration and the simultaneous space used when these operations are nested.□

Proof. If b\ge a, the usage hit is already the conditioning hit. The conditional normalization of a bin therefore turns b\mathcal B_b into its deterministic bin contribution. If b<a, nested origin boxes give

for every integrable V on the narrower slice. Thus the importance factor performs exactly the required change of conditioning.

For a fixed midpoint in Equation (7.2), first make this terminal change when necessary and then condition on Z_f(z)=1. Apart from membership indicators, the true right bin gate and denominator use only channel Y. The true left correction uses only channels X,Z. These channels are independent, and the remaining true multipliers are deterministic. The two normalizations can therefore be applied separately. In particular, after the midpoint hit is fixed, the shared role Z does not occur in the right bin’s remaining random value. This is an identity for the true atoms; the estimates will instead be compared by their joint error norms. The factor f/\pi_f cancels midpoint sampling and converts its correction atom to the correction entry. Summing midpoints proves the product formula. The projection multiplies by deterministic r_i(x) and includes the routing fraction in the bin, so the same argument applies on each fixed-symbol part. Fixed-suffix invariance in Lemma 3.1 justifies all inherited padding conventions.

The second channel is its defining preparatory conditional mean, on its own narrower slice; it has no importance factor. The detector mean is the definition of U_i. True reward factors are deterministic, so the same midpoint argument proves Equation (7.5).□

Proof. Put v=\max(H^{1/s},(H')^{1/s}) and w=\min(H^{1/s},(H')^{1/s}). Factoring v^s-w^s bounds it between v^{s-1}(v-w) and sv^{s-1}(v-w); the denominator is between v^{s(s-1)} and 2^{s-1}v^{s(s-1)}. This proves comparability. For a mixture, apply Hölder to |H-H'|=\mathcal L(H,H')^{1/s}(H+H')^{(s-1)/s} and then integrate; the triangle inequality first bounds the absolute difference of the integrals. This proves contraction, including finite sums.

If H'\le2H+a, then H+H'\le3C_0G+a\le C'(a+G), which proves Equation (7.7) directly. If H'>2H+a, then |H-H'|>H'/2, H+H'<3H'/2, and H'>a. Thus \mathcal L(H,H')\ge cH'\ge ca, while the left side is at most a.□

Proof. First suppose b\ge a. Apply Equation (7.7) after conditional expectation, and then the mixture contraction of Lemma 7.2 before it. Homogeneity supplies a factor b/a after division by a. The factor f/\pi_f in a product is bounded above and below by fixed constants. For bounded nonnegative atoms a product-root difference splits into the factor-root differences, multiplied by fixed constants times support indicators of the unaffected factor in one of the two versions.

To determine the source-domain factor, write \Delta_s\mathcal F and \Delta_s\mathcal B_b for the root discrepancies. After integration on the source/end slice, the relevant sums, besides O(b/a)/N, have the forms

Either support indicator can come from either compared version. In the first sum the right row cap eliminates y at constant cost. In the second sum the left incoming cap eliminates x at cost O(1/u). The right child’s row metric has weight 1/f, leaving exactly O(f/u). Its tuple is the same for every old source, so this elimination compares the same right error throughout. More explicitly, for either left support relation \mathcal P with incoming degree at most K_c and a common right discrepancy e(z,y), the relevant inequality is

where the source channel in the last norm is Z. The incoming cap applies pointwise, so the discrepancy can depend on the same environment as \mathcal P. Using Y_a\le Y_b enlarges the remaining endpoint domain to the child’s own domain. A direct term simply retains its source and endpoint sums. In a projected term, the source-multiplier error eliminates y by a row cap and changes the vertex weight from 1/u to 1/f_{\rm par}; this costs O(f_{\rm par}/u). Partitioning the fixed copy symbols keeps every tuple common during these sums.

For b<a, change the terminal conditioning to Y_b before taking a power. The normalized coefficient inside is then b/a. There are only constantly many nonzero left paths in the union of the two rows. Ordinary bounded-factor difference inequalities and the finite-sum power inequality therefore apply with constant cost. The integrated change from Y_a to Y_b leaves \pi_a/\pi_b outside the power. Its total factor is

The same row and incoming sums as above then apply, now with Y_b. Ordinary differences of bounded nonnegative values are controlled by their root differences. Absolute mean error bounds clipped relative mean error, so this proves the fine-bin assertion.

For the second raw channel, Jensen is applied directly on \mathcal C_{xy}^{u,t}. Its integrated endpoint mask is Y_t, already contained in the preparatory norm’s Y_a domain. There is no importance factor and hence no \pi_a/\pi_t penalty. The fixed scaling \zeta does not increase the cost.

A rank discrepancy is at most the supremum of its input discrepancies. For the detector trial, summing its power over Y_f/f is bounded by the score error sum over X_f/f and Y_f; the rates match exactly. For rewards, the finite left-path count gives an ordinary product comparison, and the same incoming cap eliminates old starts for a right-vector error. Source functions have bounded Lipschitz roots in their clipped detector inputs, so their costs are the broad vertex costs already computed. Every estimate here is pointwise or follows from Jensen and summation; none uses independence of its errors.□

Proof. The deterministic contribution H has entries at most Cb and bounded row mass. For a product these bounds follow from Lemma 5.2. Therefore

Integrating source hits gives \pi_u/u=O(1), and summing at most N rows cancels the normalization 1/N.□

Proof. A descriptor records the finitely many formula and copy-part choices, its scale and budget offsets, its sign in Equation (7.11), the generator word and guessed wraps, and a bounded number of constituent ports. An included scale obeys |h_b|=O(d), and the walk has length O(d). Lemma 6.3 therefore bounds all these records by O(d) bits. Port alphabets are fixed by Lemma 5.6. There are only O((1+d)^2) choices of budgets and scales before the exponential word/variant choices.

Check each constituent port, the outer source and endpoint memberships, and the guessed wraps at the vertices where their coordinates can be evaluated. For a fixed endpoint and original generator word, unique wrap validation leaves exactly its genuine conditional transformation. Give the surviving term its original walk-word probability, multiplied by the formula coefficients and sign. Guessed wraps do not change that probability. Constituent ports enumerate entries once. Hence summing over true equal endpoints is precisely the walk of the difference, even though its endpoint was not known when the variant was specified.

The first factor of every product is a correction, whose retained ports have bounded degree in both directions. Its paired move supplies the midpoint and a bounded return token. The right factor can then be queried using the common Z,Y tuple prescribed above; that tuple contains no old source. A direct unbalanced terminal motion has no further factor query at its endpoint. These are combinatorial access requirements; the controller section implements the pairing and terminal operations. Finally, the slack definition gives m\le M-d, also for the m-1 term.□

Proof. Available scales. For an available scale, conditional expectations of Equation (7.11) telescope to its term at m=m_j(b) in Equation (7.12). If this budget is zero, the term is zero and the inactive-child bound still applies. More generally, the child bound remains valid whenever its precision is nonpositive, by the bounded-output estimate for inactive tasks. In every case

Choose K_{\rm prec} so that c_0/K_{\rm prec}<1/8. Equation (7.10) is then bounded by

The rate grid is geometric, so summing this bound over available scales costs a fixed constant. There are only a fixed number of formula and factor types. Unbinned calls use the same calculation without the scale sum. Minkowski and subadditivity of clipped relative discrepancies combine all these terms. Exact base contributions are already present in every prefix and have no error.

Wholly omitted scales. A bin with c_b\ge M contributes no layer. We bound its deterministic contribution directly by Lemma 7.4. First we show that every such bin is fine. Put r=\log_2(1/a)\ge0. A coarse bin has 0\le h_b\le r because all grid rates are at most one. Activity gives M>K_{\rm prec}(r/2+A_*i_*), even after discarding the nonnegative start-rate cost. With K_{\rm prec}/2>c_0 and A_* sufficiently large, this implies M>\lceil c_0(1+r)\rceil, so a wholly omitted bin is fine. For the sparse direct term b=f, the same argument gives availability when f\ge a. When f<a, the admissibility condition a\le K_f f gives |h_f|\le\log_2 K_f, and increasing A_* ensures M>c_f. Thus this term is never wholly omitted in an active task. The inequality c_b\ge M implies

Lemma 7.4 and a geometric sum consequently bound all such omissions by C2^{-(s-1)M/(s c_0)}. Since p\le M/K_{\rm prec} and K_{\rm prec}>s c_0/(s-1), this is at most C2^{-p-\eta M} for some fixed \eta>0, after absorbing the fixed rounding offset. Finally M>K_{\rm prec}A_*i_*\ge K_{\rm prec}A_* makes its coefficient arbitrarily small as A_* increases. Taking, for example, any fixed B_1>1/K_{\rm prec} proves the claim, including every last-budget and no-budget cutoff loss.□

Proof. Subtract the same stochastic true-atom term from the budget-m and budget-(m-1) terms, and use the triangle inequality. A product has only constantly many left paths in the union of the compared rows. Ordinary bounded-factor differences and the row and incoming caps therefore give the sums used in Lemma 7.3, without any averaging. For a coarse bin the absolute coefficient costs b/a in the norm rather than its s-th root. For a fine bin the importance factor can stay inside the power. Both are bounded by 2^{O(|h_b|)}. Equation (7.9) pays the only separate possibly large domain ratio, f/u, as before. All other scale and accuracy changes are 2^{O(d)} because |h_b|=O(d) and M-m=O(d) in this group. Ranks and bounded source functions obey the same pointwise comparisons. This proves Equation (7.13). Replacing comparison to truth by a comparison of the two coupled child versions gives the second assertion by the identical inequalities; independence is still unnecessary.

For a fixed guessed variant, valid paths require the transformed memberships. Change variables by its full-environment measure-preserving bijection and then discard surplus validity guards. This leaves exactly the child-domain sums just bounded. When combining the paired terms, combine their contributions at the same actual endpoint before measuring the difference. The number of distinct variant descriptors is 2^{O(d)}, so treating them separately merely enlarges the crude exponent. The estimate before such separate counting is a statement about the single-seed sample function and has no dependence on the eventual walk length coefficient.□

Proof. The mean assertion is Lemma 7.6. For a difference layer, write F_{xy} for its sample function on \mathcal C_{xy}^{u,a}, \mathcal A_{xy} for the conditional walk operator of length \ell(M-m), and \Pi_{xy} for uniform averaging on that slice. Put w_{xy}=\Pr(\mathcal C_{xy}^{u,a})/(Nu) and r_{M-m}=C2^{-c\ell(M-m)}. Lemma 6.2 gives a uniform operator bound, so

The slice weights make the sum on the right precisely the integrated raw norm to the sth power, bounded by Lemma 7.7. Thus the uniform operator estimate applies directly to the integrated input bound, even when different slices have different input norms. For the second channel replace Y_a by Y_t in the slice and its weight; the mask stays Y_t throughout. Vectors use the same calculation on their one-vertex slices. No extra conditioning factor appears.

There are O((1+d)^2) budget/scale terms in a group. Choose \ell so that the contraction dominates 2^{C_0d} and this polynomial, leaving at least 2^{-(K_n+1)d}. Summing groups with slack at least d_j gives Equation (7.15). Exact base terms have no noise. This contraction applies to the paired difference as one function of the same seed. The sum of valid variants is the conditional walk, so the gap applies to that sum before any separate variant counting. Increasing A_* supplies an arbitrarily small coefficient in both this estimate and the mean bound.□

Proof. The zero-radius assertion is immediate. Since z'\leq3u_0, if m_y\geq3u_0 then

which proves identity there. Clipping a displacement toward zero proves the coordinatewise assertion. Also z'\geq u_0\geq z.

If two input arrays and their defaults differ by at most \delta, their size arrays, size ranks, u_0’s, and q_0’s differ by at most \delta. Their new defaults differ by at most 3\delta, and their clipping radii by at most 21\delta. The elementary bound

therefore gives, for example, a Lipschitz constant 28 for the full update. This constant is independent of the number and magnitudes of entries.

Fewer than n_j positions have size strictly larger than u_0. A coarse test supported above u_0 and full above 2u_0 retains all possible exceptions within the stated cap. A position outside the old list and new candidate set has input (z,0), has size at most u_0, and hence becomes the new default. No other position need be inspected. The selected list may retain some real positions that become exactly default after compression. Such positions still represent the same full array. No padding dummy is selected, since its input size is at most u_0.□

Proof. The uniform preloss bound follows by adding the changes described above. If a change occurs at group i at a position with d_y\geq\eta, then |w_y^1|\leq3\rho_i and the preceding preloss is much smaller than \rho_i. Thus

The change of size at most 6\rho_i is consequently bounded by C\rho_i e_i(y). Adding such changes proves Equation (8.9).

In the reference array negative first magnitudes and all second magnitudes are at most \eta, by the choices of \zeta and the floors. Let q be its initial Kth first-coordinate rank. The default is nonnegative, so q\geq0. If q>\eta, then n_i\geq K implies that the n_ith size rank is at most q. The floor and preceding default are also at most q, so u_0\leq q and z'\leq q. Entries at most q stay at most q. Entries at least q are unchanged if q\geq3u_0; otherwise z'=q, and they stay at least q. The Kth rank is therefore unchanged. Negative first magnitudes and second magnitudes do not grow, so this argument repeats at every subsequent group. If instead q\leq\eta, the size rank, u_0, and new default are at most \eta, and the next Kth rank is again at most \eta.

Consider an individual row function. In the first case its rank stays fixed. If its gate is not already zero, q<g_H, so every entry in its support has first coordinate greater than e_H>3q\geq3u_0 and both channels there are untouched. A position below entry support cannot cross into support because the default is at most q<e_H. In the second case the rank stays in the common full-gate region; the same identity argument applies to every position in entry support. Thus each reference output is preserved.

Finally, positions with d_y<\eta stay below every entry threshold and cannot change a rank within its sensitivity region. Perturbations at all other positions satisfy Equation (8.9). Clip first entries and ranks to the fixed sensitivity ranges and use root-Lipschitz continuity of the row functions. This proves the last assertion.□

Proof. Write E for the sum in Equation (8.11) without the initial constant. If E exceeds a sufficiently small fixed constant, bounded output ranges suffice. Otherwise all clipped errors involved are strictly below 1. Hence

and later increments have first magnitude at most (1+d_y)(e_i+e_{i-1}) and second magnitude at most e_i+e_{i-1}. The input difference at group j is precisely S_j-(d,v); both calculations include the same previous preloss. The factors 1+d_y prevent a direct absolute-error bound with a uniform constant when a true entry is large. The following two cases use the row gate and saturation to remove that dependence.

Choose G larger than every gate close threshold. A baseline at least G closes all gates, since the dummy entries force every first-coordinate rank to be at least the baseline. Closure is permanent under the unclamped update. Choose L_0 much larger than G, all sensitivity thresholds, and 1. If at least K true first entries exceed L_0, the reference gates are closed. In the perturbed calculation either some u_0\geq G, which forces permanent closure, or every u_0<G. In the latter case those K coordinates stay larger than half their true value: their initial error and the total later additive variation are at most C(1+d_y)\sum_{i\geq j}e_i, and their first value is then larger than 3G. Inductively each such position lies in the compression identity region. These K positive entries close all gates as well.

It remains to consider the case of fewer than K true entries above L_0. Lemma 8.2 bounds every reference rank and threshold by 2L_0. Fix L_1 much larger than L_0 and all upper saturation thresholds. At the at most K-1 positions where d_y>L_1, replace the first input at group j, in both calculations, by one common positive sentinel larger than L_1, and give that coordinate zero later first-channel increments. Do not modify second channels. The reference ranks, thresholds, and outputs are unchanged: these coordinates stay above the relevant ranks and in all upper saturation regions. The sentinels are comparison devices in this proof. They need not be identified or stored by the compression algorithm. Fewer than K such coordinates occur, so replacing them by common large values removes their possibly large absolute differences while preserving every rank that lies in a sensitivity range.

All remaining first-coordinate input errors and increments now have absolute bounds by C(1+L_1)e_i and C(1+L_1)(e_i+e_{i-1}), respectively. Lemma 8.1, iterated from j to the last group, therefore bounds every array and threshold discrepancy by CE, on taking C_1 larger than the fixed update constant. If E is sufficiently small, all these thresholds remain below 2L_0+1. The final root-output discrepancy is at most CE.

To remove the modification in the perturbed calculation, argue inductively. Every original coordinate with d_y>L_1 remains above d_y/2, because its total raw additive variation is at most C(1+d_y)\sum e_i. It is thus above the bounded thresholds and in the identity and saturation regions. Replacing fewer than K such positive coordinates by sentinels cannot change either a Kth first rank or an n_ith size rank whose sentinel-computed value is at most 2L_0+1: both the original and modified values are above that bound, and n_i\geq K. The defaults and thresholds therefore agree, the compression is identity in both channels at these positions, and all other coordinates agree. The relevant output behavior is the same. This completes the induction and the proof.□

Proof. By Equation (8.1), the deterministic heavy set

Conditional on one specified endpoint hit, each other endpoint in this set is retained with probability at most Ca, by Lemma 3.1. This remains true if the specified hit uses the narrower rate. The forced endpoint contributes at most 1, so the expected retained heavy count is at most 1+Ca|A_j(x)|\leq C'/\rho_j. The independent start condition has no effect. Markov’s inequality at the threshold n_j/2 proves Equation (8.13). This calculation uses the conditional pair bound and linearity of expectation; it permits dependence among the heavy-endpoint hits.

For the first-channel mean error at a fixed row and endpoint, write its deterministic magnitude as b_i(y). Then

Condition on the start and that endpoint before taking expectations. Equation (8.13) bounds the resulting expectation by C/(n_j\rho_j) times the endpoint-integrated mean-error power. Indeed the factor b_i(y)^s is fixed under this conditioning, so

The second-channel mean error has a deterministic magnitude multiplied by Y_t(y); repeat the same argument using the narrower conditional bound. Taking roots and using Equation (8.4) proves Equation (8.14). The conditioning step uses the deterministic mean-error magnitude at the specified endpoint. Prefix noise can depend on the heavy-count event, so no analogous conditional estimate is asserted for it.□

Proof. Equation (8.2) converts every row sup bound above into a bound for its summed output power with a fixed factor. In fact the support of a discrepancy lies in the union of the true and computed supports, whose total size over \mathcal H is at most 2C_{\mathrm{supp}}. Thus this step introduces no factor from the ambient number of endpoints. The preloss contributions have norm at most

On the event of no overflow, Equation (8.10) adds the final-prefix cost, at most Cc_*2^{-p}(2^{B_1}+2^{-K_n}). By Equation (8.12) and the disjointness of the possible first-overflow events, the total false-type error power is at most

For a true-type first overflow at j, use Lemma 8.3 and split e_i\leq\beta_i+\gamma_i. For the mean part, enlarge the actual first-overflow event to \Theta_j, apply Equation (8.14), and use Minkowski’s inequality. Its total norm is bounded by

For the noise part, use the uniqueness of the first-overflow group on each row. Its tail noise sum is bounded pointwise by the single full sum \sum_iC_1^{m_*-i+1}\gamma_i, regardless of dependence between noise and overflow. More explicitly,

because at most one indicator on the left is nonzero. The absolute prefix-noise bound therefore gives norm at most

without an extra sum over j.

Choose c_1>B_1 large enough for the floor conditions. Choose c_2>sc_1+sB_1 with a fixed positive margin and also large enough that n_j\geq K. Equation (8.16) then converges uniformly. For its mean term the exponential factor is exactly 2^{-(c_2-sc_1-sB_1)d_j}. For Equation (8.17), its inner sum is at most C(d_j+1)^A2^{B_1d_j} for a fixed A, by Equation (8.7) and dyadic grouping; the stronger choice of c_2 just made ensures convergence of the outer sum, whose exponential factor is 2^{-((c_2-c_1)/s-B_1)d_j}. Taking K_n sufficiently large handles Equation (8.18). The preloss sum converges by c_1>B_1. All constants are fixed before choosing the arbitrarily small prefix coefficient c_*, giving Equation (8.15) and the asserted spare coefficient.□

Proof. Compare the clamped and unclamped calculations with the same increments. For the fixed level G<L/10, once both baselines are at least G, all gates are zero because of the dummies, and remain so: compression cannot lower the baseline and every clamp bound exceeds G. It remains to compare the calculations before this happens.

Maintain the following invariant. Their baselines agree while below G. Their coordinates either agree, or have matching signs and magnitudes well beyond L; any such differing component has enough remaining margin that the total future increments cannot bring it into [-L,L]. At the first clamp of a component this follows from Equation (8.19). A subsequent clamp restores the same margin using the current R_i. Between clamps, common additions consume at most the available tail margin.

After an addition, entries whose components differ therefore have size larger than L in both calculations. Their size-rank statistics either are equal below G or are both at least G: differing values lie above this comparison range and all other size values agree. In the latter case both new baselines close the gates. In the former case the two values of u_0 agree and are below G. Only the first-coordinate rank clipped at 3u_0 is needed to compute z'. Differing positive first components are above this range; differing negative first components are below zero and do not affect its nonnegative clipped value. Consequently the two new baselines agree as well. If this baseline is at least G, both calculations close. Otherwise every differing position lies in the compression identity region because its size exceeds L>3G; equal coordinates at other positions undergo the same update. Thus the invariant continues.

Before closure, all rank arguments and all entry arguments within their sensitivity ranges agree. Differing large components have matching signs and identical saturated behavior. The final row functions therefore agree. A scalar clipping map is 1-Lipschitz, which gives the comparison assertion. For a vector sum, the same tail-margin argument ensures that a clipped value stays on the same saturated side until the final bounded clipping; no rank argument is needed.□

Proof. To apply Proposition 8.5, use the deterministic-mean and absolute-noise bounds of Lemma 7.8. The first target is nonnegative with bounded deterministic row mass before division by a, and its second target is bounded by a fixed multiple of \zeta and vanishes below the preparatory support threshold. The buffered row functions and their witnesses have fixed root Lipschitz constants and fixed support bounds. These verify its remaining hypotheses. The compression proposition shows that all their errors are a fixed multiple of c_*2^{-p} when its convergent series of floors, capacities, and noise weights are chosen. This includes the pre-incoming quantities required by the incoming comparison. Exact endpoint grouping gives common increment arrays for the clamped and unclamped calculations. Lemma 8.6 therefore preserves these row-function values, including scores and witnesses, so the same estimates hold after clamping.

Lemma 5.7 then charges the incoming gates by those same pre-output norms. Its separate column-vector calls have a fixed positive budget slack and decrease task rank. Equation (7.9) pays their broad-domain factor, and increasing A_* makes their remaining coefficient as small as required. A final vector needs no compression; its clipping is nonexpansive and the bounds at d_j=1 apply directly.

Choose the fixed atom range/support bound C_b first. Choose c_0 and K_{\rm prec} to retain the margin in Equation (7.10) and fix B_1. The compression proof then chooses its floor exponent c_1, capacity exponent c_2, and required noise decay K_n. Choose task separation and walk length sufficiently large to supply the needed small c_*. The total coefficient can thus be made at most C_b/2. Inactive tasks retain their separate trivial C_b bound. The remaining half of the active-task error bound is reserved for the coupled fingerprint error.□

Proof. Pad all encodings to the same length and put P_v(T)=\sum_{i=0}^{L-1}v_iT^i. Choose a prime B^3\le q\le2B^3, increasing the fixed lower bound on B if necessary. Thus L<q. Let \ell=\lceil\log_2q\rceil. Split a string of 3\ell fair bits into independent integers R,A,C in \{0,\ldots,2^\ell-1\}, and reduce them modulo q to obtain r,\alpha,\beta. Each residue has probability at most 2/q. Let \tau:\mathbb F_q\longrightarrow\{1,\ldots,B\} partition the standard residues into consecutive sets of sizes differing by at most one, and set

All computations are in \mathbb F_q before applying \tau.

The nonzero polynomial P_v-P_w has degree at most L-1, so it has at most L-1 roots. This root bound follows by repeatedly factoring T-r_0 at a root; it applies here because the coefficient difference 1 or -1 is nonzero in \mathbb F_q. Consequently

For distinct evaluations z,z', the map (\alpha,\beta)\mapsto(\alpha z+\beta,\alpha z'+\beta) is a bijection of \mathbb F_q^2. Under uniform parameters its two outputs are uniform and independent. The probability that their \tau-values agree is

The actual joint law of (\alpha,\beta) is pointwise at most four times the uniform law and is independent of r. Adding the two cases gives 2(L-1)/q+4/B+4/q=O(1/B). A polynomial evaluation by Horner’s rule and the residue arithmetic use O(\log q)=O(\log B) bits. The prime can be chosen uniformly by searching and trial division in that space. The existence of a prime in the indicated interval is the same elementary prime-interval fact used in choosing the environment field.□

Proof. Induct on the budget and, within a task, on its prescribed sequence of operations. Lower-block algorithms ignore the salt of block b and later salts by the access rule; same-block clean children ignore them by induction. Candidate tests use these children, exact endpoint grouping precedes compression, and the compressed row determines its exposed classes and pre-incoming scores. Incoming ranks use those completed scores. Separate column-vector queries likewise use a smaller-budget clean child in this block or an actual child below it. All statements here concern the current effective environment: each same-block transformation preserves its current and later salts, and each lower-block transformation acts on a subset of its earlier salts. Each numerical recipe uses the same fixed operand order, and each structural test uses its fixed accuracy level and tie rule. Its result therefore depends only on earlier clean operands, including their finite numerical approximations. The fixed index orders then give salt-independent representatives and ports.

In particular, exact full-array addition, compression, and the prescribed row functions are salt independent. Reordering paths or choosing a different representative of the same endpoint would not change an exact sum; retaining an extra default-valued position would not change the represented array. The fixed conventions above also remove these presentation choices from the structural calculation.

For a group with d>2h_*, every child budget is at most M-d<M_b. Both runs use the same lower-block children and exact comparisons there. All their list operations, including their deterministic tie conventions, ignore the present salt. Thus their boundary states agree. The last larger dyadic slack, if there is one, is at most 4h_*, so its shortlist has at most 2^{O(h_*)} positions. If there is no larger group, the boundary list is empty.

Finally, the clean estimand depends only on rank channels and earlier salts. These are precisely the variables averaged by its conditional walk, subject to its stated vertex conditions. Same-block salts are irrelevant, and lower-block salts are free variables of this walk. Projection onto the uniform measure of the slice therefore gives a deterministic quantity at its indicated pair or vertex, with the prescribed retained-domain masks. In particular, no random dependence on a frozen salt remains in this mean. For the second channel, its deterministic mean magnitude is extended by its prescribed narrower endpoint mask, as required in Section 8. The salt rule is required of all access operations, including inverse queries and port orders; Lemma 11.11 supplies its implementation. Lemmas 6.2 and 6.3 therefore apply to this function. This verifies the deterministic-mean hypothesis of Proposition 8.7; it does not assert independence between errors of different children.□

Proof. Each fixed variant is independent of the present salt and leaves it unchanged. Lemma 9.2 therefore makes its clean witness supports \mathcal G_b-measurable. We use these supports as sets of actual IDs, not the order of a port enumeration. At a group of slack d there are 2^{O(d)} immediate descriptors, including variants, difference parts, and copy choices. The number of endpoints contributed by a direct witness is bounded. A two-factor path contributes a bounded number of left witness midpoints and, for each, a bounded number of right witness endpoints. Summing over the dyadic groups with d\le2h_* and adding the boundary list proves the size bound. No incoming bound on a clean witness is used here.

Clean exposed ports lie in their clean witness supports. Apart from the boundary representatives, exact updates can therefore create nondefault values only at the included endpoints. Compression maps all untouched default positions to the new default. Any extra exact-default slots in a shortlist may be omitted when describing its full array. This proves the representative claim. Equation (9.5) is now the pair union bound from Lemma 9.1, conditional on the fixed envelope.□

Proof. An actual endpoint outside the envelope has an offending path factor. For a direct path its actual port is outside the clean witness support. For a two-factor path, either its actual left port is outside its clean witness support, or its midpoint lies in that support and its actual right port is outside the corresponding clean right witness support. At the offending port the actual witness is one and the clean witness is zero. Thus the indicator of this event is at most the s-th power of their root discrepancy there. Union bounding over candidate paths gives a sum of such nonnegative powers. The unit-witness property holds also for exposed zero-weight ports; no lower bound on the candidate’s increment is being assumed.

Each output under consideration is bounded and has bounded row support. The union of the two output supports is still bounded, by Equation (8.2). Hence its entire row error power on \mathcal F_x is at most a fixed multiple of \mathbf1_{\mathcal F_x}. We charge this row-failure indicator, rather than the size of the offending increment. There is no endpoint sum left on the output side to pay for.

The right-factor charge is the case where the old start must be summed out. Fix a guessed variant and a two-factor path x\to z\to y. Change variables by its measure-preserving transformation, as in Lemma 6.3; in the following display all memberships, ports, and witness values are evaluated in that transformed environment. Write e_R(z,y) for the root discrepancy of the two right witnesses and \mathcal P^{\mathrm{ac}}_L for the actual left exposed-port relation. The candidate’s validity retains X_u(x), Z_f(z), and the right child’s endpoint membership Y_{a'}(y). Dropping only surplus guards, the right-port contribution is at most a constant times

The middle inequality uses the incoming cap of the actual left port relation. It does not use a clean incoming cap. The right task’s tuple is independent of x, so the same discrepancy is being summed when the old start is removed. This condition is necessary for the displayed equality with the right metric. For the fixed variant and copy part, the right tuple has only the prescribed task parameters and transformed environment. The midpoint z is its vertex argument, and the old source x is not a parameter. Its final gate and column queries use that same effective tuple, rather than the ancestral descriptor that happened to discover the entry.

For a direct or left offending port, sum the child’s witness discrepancy over its own row and endpoint domain; the bounded number of possible right ports incurs only a fixed factor. Projected paths are partitioned by the fixed copy symbols, with constant multiplicity. Normalization and preparation dependencies make the same direct witness comparison. If a candidate arose from a narrower terminal slice, its validity mask may be dropped in this row-event estimate. Thus no factor \pi_a/\pi_t is incurred. In contrast, the transformed source hit cannot be omitted before the change of variables and the incoming-cap sum; it has been retained in Equation (9.7).

At slack d, scale ratios, variants, and immediate path counts cost at most 2^{O(d)}, as in Lemma 7.7. The possible reset factor in Equation (9.7) is absorbed by the precision gain. Admissible row tasks have u\le f, as specified in Section 5. Equation (7.9) gives, after the scale-dependent O(d) terms,

Take s-th roots and use Minkowski to sum the charges. A child below M_b is identical in the two versions and contributes zero. All remaining children satisfy m\le M-d and belong to \mathcal I_b, which proves Equation (9.6).□

Proof. When all envelope keys are distinct, the rule gives exactly the actual true-ID increment: each old occurrence is updated at its own ID, and each genuinely new ID has its own bucket. Thus the discrepancy is simply \Delta_{\mathrm{ac}}-\Delta_{\mathrm{cl}}.

When there is a collision, each updated representative receives a sum of increments at at most k_d distinct actual addresses. Its magnitude is at most k_d\sup_y|\Delta_{\mathrm{ac}}(y)|. At positions not updated it is zero. At either type of position subtracting the clean increment costs at most a further \sup_y|\Delta_{\mathrm{cl}}(y)|. Apply

to obtain Equation (9.8). This also covers an increment duplicated at several old representatives and a missing increment at an unchosen new representative.

At no point are old values combined or moved to a different ID. An unlisted old position has exactly the old default, and a newly selected representative starts with that value. Therefore the full-array comparison before compression is the old discrepancy plus the increment discrepancy just bounded. There is no term involving the height of an old value multiplied by a collision indicator.□

Proof. For each small dyadic group, let \Delta_d^{\mathrm{cl},\nu}(x,y) be its complete clean true-ID increment in channel \nu\in\{1,2\}, including any exact base term assigned to that group. Take an absent second channel to be zero, and choose a deterministic descriptor bound k_d\le2^{Cd}. By Lemma 7.7, the clean paired increments at a group of slack d obey their crude absolute estimates in the retained endpoint metric. These estimates hold for each fixed valid variant after its measure-preserving change of variables. Counting variants and summing difference layers by the triangle inequality costs 2^{O(d)}, without using walk contraction. Within each paired layer the true-ID cancellation is performed before this inequality is applied. If a local unpaired base term occurs in a small group, its first-group slack satisfies M=O(d), so the same crude bound holds in its normalized raw units. Since \sup_y|Z_y|^s\le\sum_y|Z_y|^s over actual ID positions, the row norm of \max_\nu\sup_y|\Delta_d^{\mathrm{cl},\nu}(x,y)| is at most 2^{-p+O(d)}.

Lemmas 8.1 and 8.6, together with Equation (8.7), propagate an input discrepancy at slack d to the final array with a factor polynomial in d+1. At each step the discrepancy is measured between the clamped full arrays, including their defaults. The next bucket increment is compared by Lemma 9.5; compression then applies its uniform Lipschitz bound and the common clamp cannot enlarge the discrepancy. This recurrence does not require their later bucket distributions or stored lists to agree. Root-Lipschitz row functions and bounded final support then give the same type of bound for the output metric. Choose fixed C_P,A_P so that C_P(d+1)^{A_P} bounds this propagation. For a retained row define

Set H_x=0 when X_u(x)=0. This quantity bounds the propagated clean-height terms in Equation (9.8). The preceding estimates give

All increments defining H_x are clean, and its other factors are deterministic. Thus H_x and \mathcal E_x are \mathcal G_b-measurable. Conditioning on this sigma-field gives

The row membership X_u(x) is also \mathcal G_b-measurable. Integrating the last inequality in the row measure therefore yields

Taking roots proves Equation (9.9) after enlarging C. We have not conditioned on \mathcal F_x^c in this independence calculation: the actual error there is bounded by \mathbf1_{\mathcal C_x}H_x, which is then integrated on the whole space. Conditioning on the salt-dependent stay-inside event is unnecessary and could destroy the stated independence.

For the first term of Equation (9.8), split products using bounded-factor differences, actual or clean row caps, and the actual or clean incoming cap of the represented two-way factor, exactly as in Lemma 7.7. These are comparisons of unaliased sums using the respective children; they make no assumption about key success or independence of child errors. Fixed valid variants, scale costs, and counts are all at most 2^{O(d)}, with the possible source-release factor absorbed by the same precision gain as in Equation (9.7). Compression propagation is again absorbed in 2^{C d}. This proves the remaining assertion.□

Proof. Perform strong induction on the statistical budget, simultaneously for the actual target estimates, the block-clean target estimates needed at that budget, and Equation (9.10). An inactive task returns the same zero outputs and empty paths in both versions, so its coupling error is zero. Lower-block children are identical in a block coupling and already have their actual target bounds. Same-block clean children have the clean target bounds at smaller budgets. Therefore Lemma 9.2, the prefix estimate, and the compression analysis give the clean active target bounds with the spare constants in Proposition 8.7.

For the coupling, Lemmas 9.4–9.6 bound the pre-incoming quantities. Incoming gates are then compared by their rank and root-Lipschitz bounds. In their multiplier effect, restrict to the union of the final supports of the two tables; these have bounded incoming multiplicity. Thus Lemma 5.7 costs only a fixed factor on pre-incoming errors. Its separately queried column vectors have a positive constant budget drop and their f/u metric factor is covered by their precision gain. Vector raw sums have no endpoint grouping, but their same-block children may differ. The same crude individual-variant comparisons and nonexpansive clamps bound those differences. Detector rank comparisons are already part of the assembly estimate. No simultaneous key-success event over an incoming search is required.

Collect the finite number of output types and absorb their fixed assembly factors into one fixed exponent C. For a child budget m\in\mathcal I_b used at group slack d, we have

For a separate post-assembly query with constant positive budget drop, use d=1 in this inequality. Replacing the dyadic group sum by the larger sum over positive integers, all coupled child charges are at most

Counts of budget layers and dependency types are included in 2^{C d}. Groups with larger slack have identical children and contribute zero. Together with Equation (9.9), this is the complete coupling recurrence.

Choose D_2>C so large that the infinite geometric sum in Equation (9.12) is at most 1/4. Then choose D_1>D_2+1. Finally choose rational \epsilon>0 so small that

Since h_*\le\epsilon\log_2B, the direct relative charge satisfies

after increasing the fixed minimum B to absorb any fixed coefficient. The child and direct charges fit within Equation (9.10), even with room for fixed norm conventions already included in C.

Moreover 0\le M-M_b<h_* implies

This is uniformly as small as required after the same minimum-size padding. The triangle inequality therefore adds the coupling bound to the spare clean active bound, for example C_b2^{-p}/2, without exceeding C_b2^{-p}. Inactive target bounds are the previously fixed bounded-range bounds. This completes all three inductions.

The order of choices is consequential. Fix the analytical hierarchy, table thresholds, and trivial-case bound first. Choose the precision and cutoff constants for the mean comparisons; then the compression floors, capacities, and walk lengths so the clean sums converge with their spare coefficients. Fix clamping ranges and the crude exponents in the fixed-variant comparisons next. These choices determine C. Only after them choose D_2,D_1,\epsilon as above. Thus reducing \epsilon to obtain the direct collision gain does not alter an earlier clean-coefficient requirement.

Later choices of the common stage-size bound, top-budget coefficient, and environment-field exponent do not change this crude exponent C. Immediate descriptor counts depend on relative slack, fixed support bounds and fixed walk length. The sampler gap is uniform in both field size and the length of its single free-bit component. Likewise, an enlargement of the fixed identifier-length coefficient only changes the polynomial-evaluation collision term in Lemma 9.1 to at most 2c_{\mathrm{ID}}/B^2; increasing the fixed minimum B\ge c_{\mathrm{ID}} bounds it by 2/B. These enlargements can therefore be absorbed after D_2,D_1,\epsilon have been fixed.□

Proof. Proposition 9.7 adds the actual–clean discrepancy to Proposition 8.7 with its spare constant. The inactive-task bounds follow from the fixed bounded ranges and supports. The induction in Proposition 9.7 includes both kinds of tasks and every prescribed output. Applying its ordinary vector statement to W_l and taking the s-th power gives Equation (9.14).□

Proof. Starting with result bit r_0, perform the following four excursions: flip V_{k(v)}; xor V_{k(w)} into the result; flip V_{k(v)} again; xor V_{k(w)} into the result again. The key is evaluated only at the endpoint currently visited. If V^0 is the incoming vector, the first read equals V^0_{k(w)}\mathbin\oplus\mathbf1_{k(v)=k(w)} and the second equals V^0_{k(w)}. Thus the final result is r_0\mathbin\oplus\mathbf1_{k(v)=k(w)} and both flips restore V^0.

For nesting, use induction on the well-founded procedure order. A nested call sees some arbitrary incoming vector, restores precisely that vector, and returns a result independent of it. Hence the four outer endpoint paths and their keys are the same on repeated visits, even between the two outer flips. The terminal evaluation, read, or flip is a local operation with no further structural call. Only a phase and a result bit must survive across the excursions; a key index is recomputed at each visit in shared scratch. The result bit being accumulated is not used to choose either endpoint path. These facts give the induction invariant and the claimed local storage bound.□

Proof. Writing e_t=N_t-2^tz gives z_t=e_t-2e_{t-1} for t>0, hence |z_t|<6; the weaker alphabet bound |z_t|\leq6 is convenient throughout. At place zero, |N_0|<3, so |N_0|\leq2. The partial sum through place T is 2^{-T}N_T, which tends to z by Equation (10.3). Finally, reduction modulo 2^q is injective on the possible signed digits because 2^q>12. Thus the signed difference can be recovered from the two residues without forming the full integers N_t. Concretely, for t>0 compute (N_t\bmod 2^q)-2(N_{t-1}\bmod 2^q) modulo 2^q, then use the fixed finite table which sends each occurring residue to its unique representative in \mathcal A. At t=0, decode the residue of N_0 in the same way. This final decoding has constant storage and introduces no comparison of unknown exact real numbers.□

Proof. At a gate, save its next-child or return mode and the already computed Boolean input, if any. At a conditional gate also save the selected branch bit. The bounded fan-in makes this a constant-size record. To locate the next child, scan the saved path from its root and regenerate successive gate descriptions in scratch. The final description determines the next child choice. On return, its Boolean result is combined with the saved bit and the local record is popped. All temporary addresses and scan counters are discarded before an operand query; a later scan recreates them from the same root and saved choices. Circuit acyclicity gives termination. This is an evaluation of the circuit unfolded into a formula; repeated gates are recomputed, so no array of previously computed values is stored.□

Proof. First consider comparing two truncations through K=t+h, where h is a sufficiently large fixed integer. Their difference digits have magnitude at most 12. Scanning from place zero to K, update a signed prefix by p\leftarrow2p+\delta. While |p|\leq12, retain p exactly. Once p>12 or p<-12, retain only the corresponding absorbing sign state. This sign is correct for every finite continuation: the remaining suffix, in the current scale, has magnitude strictly less than 12. The state space is finite, so each transition has a fixed bounded-fan-in Boolean circuit. The sign at the end determines the exact order of the two finite truncations. The path from that sign bit to an input at place j has length O(K-j+1)=O(t-j+1).

Let v_t be the average, maximum, or minimum of the two truncations, and put N_t=\lfloor2^tv_t\rfloor. Each operation is 1-Lipschitz for the sup norm on its operands. Consequently |v_t-v|\leq6\,2^{-K}, where v is the corresponding exact output. Choosing h so that 6\,2^{-h}<1/2 gives |N_t-2^tv|<3/2.

To obtain N_t\bmod2^q, only a fixed number of low places of the selected truncation are needed. More explicitly, at scale 2^K, terms of input place j\leq t-q are multiples of 2^{q+h}. Modulo this modulus the remaining q+h places suffice. For an average with integer input prefixes A_K,B_K at scale 2^K, use N_t=\lfloor(A_K+B_K)/2^{h+1}\rfloor. Its residue needs modulus 2^{q+h+1} and one additional retained place: only places j\leq t-q-1 can be omitted. The finite number of remaining digits can be added and shifted by a constant-size Boolean circuit. A maximum or minimum first uses the comparison bit to select these residue bits. Its long comparison branch has the path bound proved above, and its residue branch reaches only places within a fixed distance of t. A fixed shift changes these places by a fixed amount. Fixed normalization factors are handled in this way whenever an intermediate range exceeds [-1,1].

The topology of the comparison chain and the low-residue circuits depends only on the root clock, the fixed margins, and the gate path. Regenerating a place by replaying that path needs no saved binary place counter at each transition. Lemma 10.2 therefore gives the suspended-space bounds. Their longest paths have length O(t+1).

For composition, use one common coefficient of (t-j) for the finite primitive list. Increasing such a coefficient by \Delta requires increasing its constant term by at most \Delta C_0, because the operand overshoot is at most C_0. With these common coefficients, the clock differences telescope along the composed path. The finite number of constant terms remains a constant.□

Proof. Fix q and write A=6. Partition ordered pairs (i,j) of nonnegative places into a zero band, where \min(i,j)=0, and positive bands

Set h_0=h_\circ for the zero band and h_D=h_\circ+\lfloor D/4\rfloor for positive bands. The fixed integer h_\circ will be chosen below. Retain in band D only pairs with i+j\leq t+h_D, and let

For the zero band the same formula uses its defining pair set. These are mathematical integers; no bound on their full binary length is assumed in the residue computation.

At any fixed diagonal i+j=s, a positive band contains at most 2D ordered pairs. Indeed the smaller place has D possibilities, and an off-diagonal pair has two orientations. The zero band has at most two pairs. Thus, in units of 2^{-t}, the total omitted product terms have absolute sum at most

The geometric summation of the diagonal weights gives this bound also when the truncation threshold lies below the first possible diagonal. Both the series in Equation (10.7) and \sum_D2^{-h_D} converge. Choose h_\circ sufficiently large that their displayed combined error bound, including coefficient 2A^2, is less than 1/2.

There are only finitely many nonempty retained bands. For a positive one, 2D\leq t+h_D, whence

The left side of the nonemptiness condition grows monotonically faster than its right side along the dyadic bands. We may therefore stop at the last band satisfying this inequality, retaining empty bands within the finite prefix if necessary.

Starting with the most distant retained band, define integers recursively by

where D^+ is the next band, and the last missing tail is zero. One internal floor, divided back to scale 2^t, changes the sum by less than 2^{-h_D}. Induction down the bands consequently shows that the difference between 2^{-h_0}F_0 and the sum of all retained terms in scale-t units is at most \sum_D2^{-h_D}. Equation (10.7) and the choice of h_\circ make the error before the final floor less than 1/2. The final floor costs less than one more unit. Therefore Equation (10.3) holds for z=xy.

We next implement Equation (10.9) using residues. At band D use modulus 2^{q+h_D}. An integer term in Equation (10.6) with i+j\leq t-q is a multiple of this modulus and can be omitted from the circuit. It remains present in the mathematical integer S_D. Only the diagonals

need to be processed, giving O((D+1)(h_D+q+1))=O((D+1)^2) candidate pairs.

Signed floor shifts are well defined on the required residues. For h'\geq h and a-b=k2^{q+h'},

This identity holds for all signed integers a,b. Thus a next-band residue modulo 2^{q+h'} supplies the correctly floor-shifted tail modulo 2^{q+h}. Apply the same observation to the final shift by h_0 to obtain N_t\bmod2^q. In the finite binary circuit, this shift just discards the lowest h'-h bits of the canonical (q+h')-bit residue. The displayed identity proves that this is valid also when the underlying integer is negative.

For completeness, the finite gate structure can be indexed without storing an absolute operand place at each gate. For a positive band enumerate triples (r,s,o), where D\leq r<2D, t-q<s\leq t+h_D, and o\in\{0,1\}. The triple supplies (r,s-r) if s-r\geq r and o=0; it supplies (s-r,r) if s-r>r and o=1; otherwise it supplies a zero term. This enumerates the relevant pairs exactly once. For the zero band use r=0 with the same orientation rule. Negative candidate places are invalid and supply zero. The offsets r-D and s-(t-q+1) have O(\log(D+2)) bits. They and o are obtained from paths in padded binary selection trees. The full places are then computed from the root clock in scratch.

Each nonzero term is a constant-bit signed product x_i y_j, shifted into a word of width W_D=q+h_D=O(D+1) and interpreted modulo 2^{W_D}. A bit of this word is a fixed Boolean function of the two bounded digit codes, the bit index and the known shift; negative products use their ordinary residue, equivalently sign extension before reduction. Add these words and the shifted tail using Equation (10.5). A band contributes depth O(\log^2(D+2)). Bit selection for the shifted tail is wiring and does not require evaluating a full tail word.

The sum of these depths through the bands up to D is O(\log^3(D+2)), hence at most C(D+1) for a fixed C. For an original input digit in a positive band, its partner place is at least D. Equation (10.10) gives

Equivalently, t-j\geq\tfrac34D-h_\circ, so the full path cost through these bands satisfies

This gives C_0+C_1(t-j) with fixed constants. The zero band has constant depth and only constant overshoot. All its gate descriptions, term coordinates, bit positions and tail shifts are computable by replaying paths and doing integer index arithmetic from t and q. Lemma 10.2 converts these depth bounds to suspended storage. Finally, Equation (10.8) bounds every intrinsic path and local word width by O(t+1).□

Proof. The input can first be normalized by a fixed binary scale. It is enough to prove the result with a fixed digit alphabet and fixed positive interval; all constants below may depend on a,b. Choose a fixed power of two C large enough that the desired output z=1/(Cx) lies in [0,1] and that the coefficients below have absolute value at most one. Put

where c is a sufficiently large fixed integer. By Equation (10.2), |e|\leq 6\,2^{-k}. Choosing c first ensures x^0\in[a/2,2b] and |e|\leq1 at every t. Increasing C if necessary gives bounded coefficients

The exact algebraic identity

shows that the linear expression T_t=\alpha+\beta e differs from z by at most a fixed constant times 2^{-2k}. Choose c large enough that

Clipping T_t to [-1,1] cannot increase this error; denote the clipped expression by \widehat T_t.

For this fixed original t, the coefficients \alpha,\beta are exact rational numbers. Their digits are produced by integer arithmetic, as described below. The suffix e has the exact stream with digit zero through k and digit x_j thereafter. Thus Lemmas 10.3 and 10.4 provide exact streams for \widehat T_t, using only a fixed number of normalized operations. Explicitly, form the product \beta e, then the pair average u=(\alpha+\beta e)/2, clip u to [-1/2,1/2] by a maximum and a minimum, and finally apply the fixed shift by 2. Every exported intermediate value is normalized, and the final value is \widehat T_t. Forming this expression introduces no additional reciprocal operation.

Let P_s(\widehat T_t) be the integer approximation furnished by those operations at place s=t+3, and define

The cutoff k and the coefficients remain those of the original t, not those of s. Equations (10.3) and (10.14) give

To obtain this integer modulo 2^q, ask for the approximation P_{t+3} modulo 2^{q+3} and use Equation (10.11).

It remains to justify storage in the coefficient computations. The signed numerator of x^0 in units 2^{-k} has O(k+1) bits. Form it by querying places 0,\ldots,k and updating the integer prefix. The numerator, a place counter, and all data that must survive the next query are part of the local record. To return a coefficient digit of place r, numerator squaring and integer division require O(k+r+1) bits. Here r\leq t+O(1), because the enclosing expression has fixed depth and constant overshoot. After the input prefix is obtained, these integer computations make no further operand queries. Standard binary long multiplication and division, performed by bounded loops with their partial products or remainder, use only this linear number of bits. For r>0, computing floors of the coefficient scaled at r and r-1 gives its exact difference digit; at r=0 use the place-zero floor alone, as in Lemma 10.1. Clipping is unnecessary because the coefficients were normalized in advance.

Every original-input query during this formation has j\leq k\leq t/2+O(1). Hence

for fixed constants, at all such queries. The enclosing gate path also has length O(t+1), so the complete suspended local record satisfies the required bound there. Equivalently, the coefficient branch is charged against the original reciprocal clock t, not against its possibly small coefficient digit place r.

On a suffix branch with j>k, the coefficient word is absent. The Boolean evaluation asks for a coefficient digit at a separate leaf, returns its bounded code bits, and discards the coefficient word. If the other child of a gate subsequently asks for a late suffix digit, only the bounded pending bits and gate choices are retained. The path bound from the preceding arithmetic lemmas therefore gives O(1)+c(t-j) also on this branch. Repeated coefficient requests rebuild the word. The parameter k and the choice of coefficient are regenerated from the original t and the saved gate path; no earlier cursor address is required. All intrinsic records have O(t+1) bits.□

Proof. For 1\le k\le n, the kth largest of the semantic n-entry list is its (n-k+1)st ascending order statistic, before any extra padding. Pad to a fixed descriptor domain whose cardinality is a power of two, adding entries of value +1. These entries do not change any of the first n ascending order statistics. An empty list or an out-of-range request returns its specified default immediately. Replace invalid original descriptors by the prescribed dummies. An operand access evaluates validity first and enters the actual value branch only when valid; an invalid access returns the dummy’s digit. Thus a dummy does not require a query to an undefined value. For each valid numerical value use its truncation through K=t+h for fixed large h. Order these finite rational values, breaking ties by descriptor index. Compare every pair using the signed comparison of Lemma 10.3. For each descriptor count how many descriptors precede it, then compare that count to the requested rank minus one. Exactly one descriptor is selected. Select its low-residue bits using Boolean AND and OR trees and finally floor to output scale 2^t. The selected descriptor is internal to this residue computation. It may change with t; the exact order statistic being approximated is fixed by the semantic list and the requested index.

If all coordinates of two finite lists differ by at most \eta, their corresponding order statistics differ by at most \eta. Indeed, at least the specified number of the perturbed entries are no larger than the original order statistic plus \eta; interchanging the lists gives the reverse inequality. Here \eta=6\,2^{-K}. Thus the selected truncation, followed by the final floor, satisfies Equation (10.3) for sufficiently large fixed h. Descriptor ties affect neither this estimate nor the uniqueness of the finite selection. This argument perturbs the entire padded exact list. Some truncated original entries may exceed +1 slightly, but their error, and hence the error of the selected padded order statistic, is still at most \eta. The padding argument requires no separate claim that every finite truncation remains in [-1,1].

Each count has O(d) bits. Carry-save counting as described above, the comparison to the requested rank, and selection among 2^{O(d)} descriptors add O(d) Boolean depth above the pairwise comparison bits and selected residue bits. A place-j input to a pairwise comparison consequently has path length O(d)+O(t-j); a residue input is within a fixed distance of t and has path length O(d). The paths to validity predicates have length at most the whole circuit depth O(d+t), and the predicates themselves are separate structural leaves of clock zero.

Each gate is specified by its pair of descriptor indices, its counting-tree or selection-tree position, and a comparator or bit position. The paths determine these indices in O(d+t) scratch, using only the fixed domain and root parameters. No numerical comparison is needed to determine the circuit topology. Apply Lemma 10.2. The constants in Equation (10.17) can absorb the fixed digit overshoot because d\geq1.□

Proof. Choose one common known power-of-two range bound for the immediate terms and divide each term by it, so every term lies in [-1,1]. Pad their number to a power of two 2^r, r=O(d), and use a complete binary tree of pair averages. Every internal value stays normalized. Along one path there are r elementary operations. Choose common coefficients in their bounds, as in the last paragraph of the proof of Lemma 10.3. The constant terms sum to O(r) and the differences of successive digit clocks telescope. Thus the local length is O(d)+b(t-j) and the total overshoot is O(d). Restore the common normalization scale only after the tree of pair averages. For a sum, combine this factor with the known padding count 2^r in one binary shift of magnitude O(d). For an average over an original domain of size m, combine the scale restoration with multiplication of the padded average by the public factor 2^r/m. With minimal padding the latter factor is in [1,2), so it requires only one normalized public multiplication and a fixed shift in addition to the common scale restoration.

More explicitly, for a shift by 2^v, truncate the operand at K=\max(0,t+v+h). If t+v+h\geq0, its scaled truncation error in scale-t units is at most 6\,2^{-h}. If the scaled output is known to be normalized, floor in the desired output scale. Otherwise, when a bounded clip is required, apply that clip to the scaled truncation before flooring. For the normalized clip to [-1,1], for example, define the approximation using \min(1,\max(-1,2^v x^{[K]})); its error cannot increase. This shift-and-clip procedure does not first export an unbounded intermediate as a normalized stream. The low residue requires the constant number of places near t+v, and a comparison needed for clipping has a constant-state chain through K. Comparisons to the scaled clipping endpoints are equivalently comparisons of x^{[K]} to the known endpoints divided by 2^v; their finite constants and shifted place data are public. When v\geq0 these endpoints belong to [-1,1]; when v<0 the normalized operand is already in the clip interval after scaling, so no clipping comparison is needed. Its path cost is O(1)+O(\max(0,t+v-j)), which is at most O(d)+O(t-j) on an actual operand query. If t+v+h<0, zero is already a sufficiently accurate approximation after increasing h, and no operand query is needed. A fixed number of such rescalings and clips preserves the bounds by telescoping. Known non-power-of-two coefficients can instead be handled as public normalized streams and bounded multiplication.□

Proof. Compute finite rational approximations \widetilde s,\widetilde u with individual errors at most \rho/16. The known range and lower bound on \rho make O(d) normalized digits sufficient. Accept exactly when \widetilde s>\tfrac32\widetilde u, using a fixed convention at equality. If s>2u, the left side minus the right side is greater than u/2-5\rho/32>0. If s\leq u, it is at most -u/2+5\rho/32<0. The finite comparison and all previous arithmetic have the bounds already proved. The test chooses its precision from d and \rho, not from an enclosing numerical clock. With its structural starting clock defined as zero, its operand requests have j=O(d); increasing a in Equation (10.17) pays also for the term -bj.□

Proof. The primitive constructions define deterministic integers N_t. Lemma 10.1 turns them into exact streams. When composing primitives, their operands are these exact streams; numerical approximation errors are not accumulated along the recipe as if they were statistical errors. Instead, each primitive’s deterministic N_t is an approximation to its own exact mathematical value. The construction uses only residues of N_t and N_{t-1} and a constant number of output code bits, which adds fixed overshoot and fixed local overhead.

For the record bound, choose one common positive clock coefficient b for the finite primitive and stage types. In any bound L\leq a_0d+b_0(t-j) with j-t\leq c_0d, replacing b_0 by b\geq b_0 is justified by replacing a_0 by a_0+(b-b_0)c_0. Thus the same b can be used everywhere. There are a bounded number of stages, each with overhead O(d); within a balanced reduction the elementary overheads have total O(d) by Lemma 10.7. Along any path the intermediate clock differences telescope, giving Equation (10.18) and total overshoot O(d). The same sum, terminated at an internal arithmetic operation rather than an operand call, gives the intrinsic bound explicitly as follows. If that operation has current clock u, its own intrinsic record has length at most C(d+u), while the outer saved portion has length at most A d+b(t-u). Choose the common b also to satisfy b\geq C. Their sum is then at most (A+C)d+bt, because u\geq0. Increasing the stage constants as above makes this same choice of b valid in all local bounds. The early-word case is already included in Lemma 10.5: those retained bits are part of the local record and are paid for at the actual original-input clock by Equation (10.16).

Structural validity branches are finite branches in this circuit organization, with length at most its full intrinsic bound. They ask the structural operand at clock zero. Buffered tests are separate recipes with structural starting clock zero and precision fixed by Lemma 10.8; they are not altered when a surrounding value is requested more accurately. Thus no discontinuous comparison of exact reals at unbounded precision is part of the interface.

All circuit constructions were given with padded domains and index rules. A saved gate choice selects an operand, a subtree, a bit of a known-width word, or one of the finite primitive modes. Scanning these choices from the root recovers the current descriptor and digit places by integer arithmetic. The reciprocal’s extra records additionally specify its early-prefix formation state. None of these computations refers to an ancestor cursor address or requires an operand value to discover the next gate. Their integers have O(B+d+t) bits; repeated scans reuse one scratch area. Lemma 10.2 therefore applies at every Boolean portion of the recipe.

Finally, for a public coefficient P/Q, Q>0, producing a place-r approximation uses integer division of 2^rP by Q, with signed floors when needed. The inputs and intermediate remainders have O(B+r) bits. Standard finite binary division and multiplication use that much space, and extracting the low residue or difference digit requires no larger word. All operand bits in this computation are public, so it makes no recursive graph call and can use shared scratch throughout. For r=O(B) its scratch bound is O(B). In contrast, any word whose bits depend on recursive operands and must survive a new operand request has already been charged to the local record.□

Proof. Use as potential states the cursor and delimited words having the specified finite tags. Check absolute parameter ranges, descriptor ranges, stage and suffix types, instruction modes, and the allowed parent-to-child recipes. Check the intrinsic word bounds of Definition 11.3. For each explicit chain also check the local bounds along that chain. Before any opaque query, check the bound from every ancestor of its local explicit chain to that query. All absolute parameters, clocks and lengths needed for these checks are regenerated or counted in scratch. No graph query is needed for a guard. At a state with an unavailable instruction omit that edge.

The designated paths pass the guards by hypothesis: their boundary bounds add along an explicit chain and telescope. Enlarging the coefficients once covers fixed instruction tags and bounded intermediate edits. The resulting graph is finite since its local words have O(w+t) bits and its cursor has O(B) bits. It is deterministic since every branch bit and partial paired map is deterministic. Guards may create additional dead ends, but they cannot create a new path from a canonical initiation to a success state.

For a local edit, predecessor candidates are obtained by guessing the bounded overwritten symbols, preceding finite mode, and bounded head moves, then testing the instruction forward. Marked positions and incremental erasure make the number of cases bounded. For a branch, perform the same fresh restoring query at the unchanged cursor and test the guessed preceding symbols. Incorrect historical branch bits do not resume the interior of a lower procedure: the query is always started again on its regenerated arguments. The guards are checked before the query, including for a candidate predecessor.

For a cursor step, first construct the possible preceding local record by a bounded inverse edit, guessing the bounded preceding token if needed. Before any motion, replay that candidate’s active records from the fixed root tuple. Check the instruction and stratum, permitted child kind, budget, scale and suffix ranges, salt permission, numerical clock and every ancestor-to-query raw length bound. These allocation and recipe checks do not use the predecessor cursor. The lower motion tuple is then fixed by the candidate record and the present output token. Apply the partial inverse at the present cursor and output token. If it succeeds, the returned token and preceding local symbols specify the candidate predecessor. Static checks and token comparisons can be made there. A guessed preceding port is compared with the actual port returned by the inverse. Any remaining cursor-specific type or domain check is pure at that cursor; a domain condition requiring another restoring query belongs to a separate branch edge. Thus it does not conceal a second high-cost query inside this paired step. To restore the probe, apply the paired forward map with that same tuple and the actual returned token. No saved copy of the cursor is used. Conversely, an outgoing paired probe checks the proposed target guards after its motion; if a guard fails, or if the probe is only a restoring incidence test, its inverse with the actual output token restores the starting cursor. Both directions have been allowed the same lower-operation cost. No unrelated value query is part of this cursor step.

Label an edge by its finite instruction case and bounded erased symbols. Its forward instruction determines a canonical reverse case code. An inverse probe accepts only that code. This removes any duplicate descriptions of the same predecessor edge without comparing two retained addresses. The finite case codes give a fixed local order and a bounded incidence token; a forward edge knows its reverse token.

For the space assertion, first ignore saved probe copies. Adding the boundary inequalities along the current explicit chain gives the bound a_0(w-w')+b_0(t-j). A current state and a candidate predecessor differ in length by a constant: this follows from the bounded edit used to construct every candidate, before it is known to be an actual predecessor. Consequently retaining or editing both costs only a fixed multiple of that bound, with a constant adjustment absorbed by the strict allowance decrease. More explicitly, write \Delta w=w-w'>0 and \Delta t=t-j\ge-a'\Delta w. For a fixed copy factor k and additive bounded metadata cost h, choose

Then k(a_0\Delta w+b_0\Delta t)+h\le A\Delta w+D\Delta t. This also handles a negative clock decrement. These coefficients are uniform over all finite instruction cases.

The constants a_0,b_0 describe the raw skeleton uniformly over the whole recipe family. They have not been replaced by the physical probe constants A,D in a lower skeleton’s guards. Fix the maximum finite copy factor k and metadata cost h and choose A,D once. A lower compiled query contributes a new physical stack segment when it runs; its contour state and saved copies are not words in the calling graph. Thus this estimate copies raw records, not another A,D-sized physical segment.

Only the local explicit chain is saved or edited. A nested query has its own root boundary and appends its local portion below the existing stack; its program graph excludes the caller’s saved copies. A tag selects the candidate chain for parameter replay, ignoring an inactive saved copy. Therefore a later neighbor probe does not copy the older outside portions again. Finally, all guards and forward case codes use just the fixed tuple and its permitted records. Imposing the same salt-visibility convention as the underlying recipe preserves this independence even at synthetic states.□

Proof. Following the unique successor from any node in the undirected component reaches its sink. Indeed a directed cycle in a graph of outdegree at most one cannot be joined by a path to a sink: at the first connection the unique outgoing edge is already used toward the cycle. Equivalently, on an undirected cycle all its vertices must use their outgoing edge on that cycle, so no sink lies in its component. The same argument excludes two sinks in one component. Thus the component is a finite tree with the given unique sink.

Take the incidences of its edges, with an additional sentinel incidence at the root. Edge flip exchanges the two incidences of an edge and fixes the sentinel. At each vertex cyclically rotate its incidences in the fixed local order. Rotation followed by flip, or its inverse, gives one contour cycle on these incidences. This follows by induction on the number of edges: inserting a leaf inserts its two incidences into the old cycle. The isolated-root case consists only of the sentinel.

At a canonical initiation mark its unique successor incidence; mark the sentinel at the root. Each initiation is therefore counted once. Iterating the contour successor to the next mark always terminates, since the finite contour contains the root mark. Iterating its inverse to the preceding mark is the inverse operation. A success tag and the sentinel token identify the root in this component; its address never has to be compared with an earlier address. Constant-degree adjacency and edge flip are provided by Lemma 11.4.□

Proof. Give invalid row ports a distinct failure execution. The canonical initiations in a success-root component then correspond exactly to valid class entries at that endpoint. Class validity is tested before using a forward initiation as a contour starting point.

Start at a valid initiation mark. Go forward toward the sentinel, counting other initiation marks, stopping either at the sentinel or after K_c other marks. Store the number of mark jumps, at most K_c+1, and restore the start by that many inverse jumps. Do the same in the backward direction and restore again. Reaching K_c other marks certifies excess. Otherwise, let a and b be the numbers of other initiations before the sentinel in the forward and backward directions. The total is 1+a+b; accept exactly when this is at most K_c. The initiation’s rank after the sentinel in forward order is r=b+1. A forward paired motion goes to the sentinel in a+1 mark jumps and returns the inverse port r.

From a canonical endpoint halt, count forward marks until returning to the sentinel or encountering K_c+1 initiations. In the latter case restore the sentinel by the bounded number of inverse jumps and reject. In the former case the total n\le K_c is known. For an inverse port r\in\{1,\ldots,n\}, go forward by r mark jumps to its initiation and return the row port stored in that initiation state. Invalid ranks are rejected at the sentinel. A halt with no preimages has n=0 and is harmless. Wrong vertex types can be rejected before creating a halt state.

Every unsuccessful inverse request therefore leaves its endpoint unchanged: an excessive incoming count is undone before failure, and an invalid rank is detected at the recovered sentinel. For a successful request the returned row port is the one in the reached initiation, not a guessed port. This is the token used by a later forward restoration in Lemma 11.4.

These are inverse maps by the common contour order. Existence tests make the corresponding visits and reverse them, so they restore the cursor. All counts, ranks and incidence tokens have a fixed alphabet. The terminal program graph has the common table tuple as its root; neither direction fixes the starting row or port as an external parameter. Consequently the two directions use exactly the same graph. Restoring lower queries restore the catalyst, and the contour itself does not otherwise change it.□

Proof. Normalize the score range to [0,1], using a fixed public factor if necessary. At approximation place t, choose a fixed extra margin c. For the digit truncation v^{[t+c]} define the integer

The digit tail has absolute value at most a fixed constant times 2^{-t-c}. Choose c so that this is less than 2^{-t}. Clipping is nonexpansive and fixes 2^t v, so |q_t(v)-2^t v|<2. The same margin gives q_t(0)=0: a truncation of the zero value has scaled magnitude less than one, so flooring and nonnegative clipping give zero. Since the forward class contains every positive score, enumerating its entries and padding by zero therefore gives the rank of the whole quantized score column.

Use a forward terminal program which first tests the entire class and membership domain at its canonical initiation, sending invalid inputs to failure. Its success configuration contains the endpoint in the cursor and q_t(v) in its local state. Before making its final structural motion, assemble the score digits from least to most significant. In units 2^{-t-c}, before the place-j digit is queried the accumulated suffix and its carry have O(1+t+c-j) bits. A self-delimiting offset from t+c fits the same bound. After assembly, division by 2^c, flooring, clipping and loop setup are pure local computations. The complete word is then held only through structural motion and local clearing to success. Thus all its graph-query boundaries satisfy the claimed record bound. The success word is part of the graph state, not a parameter of the graph. At this fixed t the graph includes every allowed quantized value.

At the requested endpoint, initialize the success state at q=2^t. Tour that root component and count canonical initiations, saturating at the desired fixed rank. Continue to the sentinel even if the saturated count has already been reached. At the sentinel the same endpoint and quantized value have been recovered; no other success halt occurs in that component. If the cumulative count has not yet reached the requested rank, decrement the value field by pure local steps and tour the next success component. The value field itself is the loop variable. No separate copy of it survives the tour. The saturated count and control bits have constant size. At value zero apply the stipulated zero padding.

If the desired rank has been reached, use the value field only after the tour has returned to the sentinel. The clock t is a root parameter throughout; the loop value q is not. Consequently an inverse step which reaches an earlier partial-suffix state replaces the current score state by that suffix state, and need not retain the final q or the endpoint address alongside it. Unique-sink recovery supplies both again when the component tour ends.

This computes the integer order statistic N_t of the values q_t(v). A uniform perturbation of a finite list changes any order statistic by at most the same perturbation, including after zero padding. Thus N_t has error less than 2 as an approximation to 2^t times the desired rank. Keep only the fixed number of residue bits needed to form its redundant digit, clear the other local data without a graph query, and return at the unchanged endpoint. Computing N_{t-1} uses its own quantization convention; the difference-digit construction needs only the bounded errors, not nested quantizations.

During a tour the live program state may be a partial suffix state preceding a high-place query. It then contains that short suffix, rather than a saved copy of the final score. Lemma 11.4 therefore also gives the required bound for inverse neighbor queries. All root components are finite, including isolated success states, and the decreasing finite value loop terminates. Fresh lower procedures and the contour preserve the catalyst.□

Proof. For a direct summand the path is a local base path, a projected child path, or a child row port. A projection stores its bounded symbol before removing it and appends the prescribed destination symbol after the child terminal motion. For a product the left factor is a correction with paired access. Its inverse token is stored at the midpoint; right-factor validity and weight queries are restoring there. The right terminal path is then the last delegation. An old prefix port delegates to that preceding prefix; after its return it requires no new graph query. These are exactly the path cases of Lemma 7.5.

There are two compiled continuations of this same terminal syntax. A one-way continuation clears its path records after performing its prescribed local completions. A visiting continuation retains the immediate choices and inverse tokens on its explicit terminal spine. After the local endpoint action it undoes the bounded completions, undoes the last delegated spine, and then uses the paired inverse token of an earlier motion. Each deeper record is cleared before invoking an earlier inverse map. For a projection, the saved symbol and prescribed append symbol give its local inverse. The identical lower paired tuple and actual returned token give the inverse of a correction move.

This is an induction on terminal delegations, not an attempt to invert an arbitrary unbalanced macro in one step. A frame stores only its own immediate descriptor, bounded choices and phase. Its returned child spine is used for local completion and the endpoint action, which make no graph calls. When a further graph query is made during rollback, the deeper spine has already been discarded. Thus the suspended records are those at the corresponding forward boundary, enlarged by bounded phase and inverse-token data. The choices can be re-created or kept on their own frame; no concatenated description of all old prefixes is passed to a new tight query.

In a restoring use, intrinsic constituent validity is checked before the visit. A product can test its right port by crossing the paired left edge and returning; this test does not use the right terminal path. Outer slice and wrap tests then use a valid intrinsic excursion. Hence none of these validity checks recursively invokes the very bucket or shortlist membership it helps to define. The endpoint action’s owner is marked in the outer frame, so its tuple can be regenerated by a scratch scan even while a descendant path is retained. The action’s result does not alter the selected paths or their undo.□

Proof. The two descriptors occupy O(d) bits. By Lemma 11.8, each endpoint can be visited and restored for a local bit or hash action. If d>2h_*, compare the O(B) identifier bits in order, retaining only the bit-position counter and bounded flags. Its counter uses O(\log B)=O(d) bits, since h_*=\lfloor\epsilon\log_2 B\rfloor with a fixed positive \epsilon and sufficient minimum padding.

Otherwise use the four visits in Lemma 9.9: flip the first key’s bit, xor the second key’s bit into a result, and repeat. The final result is key equality for every incoming catalyst and that vector is restored. Key evaluation and the indicated vector-bit action are pure endpoint operations in scratch. No key index is saved across another visit. Nested structural procedures already restore the catalyst and give results independent of its contents, by their lower operation order. The outer descriptors and all path choices ignore the accumulated result bit. The two repeated visits therefore use identical paths. This proves the same independence and restoration for the completed comparison, supplying the induction hypothesis at the next layer. The comparison mode is determined by M,d and the public block boundaries, not by the requested numerical place.□

Proof. Table 2 summarizes the records to be charged. We verify the recipes and their dependencies in the order in which they are constructed. All constants depend only on the fixed construction constants and the base machine.

Immediate paths and their values. By Lemma 7.5, a group has at most 2^{O(d)} immediate descriptors: term and channel part, scale and budget offsets, a variant word and wrap choices, bounded copy symbols, and a bounded number of factor ports. All factor budgets are at most M-d. A descriptor is stored literally in O(d) bits; it never stores a discovered endpoint. Index and range tests are pure computations. Constituent existence tests call only these lower factors. Products cross a paired left edge for right-factor tests or digits, retaining a bounded inverse port; they return after each such query. Factor digits can therefore be requested separately by an arithmetic evaluation path. No assembled left weight remains over a late right-factor digit. Source vector factors are queried at the current source, with the prescribed local projection if needed. Their numerical coefficients and the factor products use a fixed arithmetic recipe.

For terminal motion the right unbalanced path, or the direct child path, is the last delegation. This is the ordered path of Lemma 11.8. To avoid a validity cycle distinguish intrinsic constituent existence, intrinsic motion or excursion, and outer validity. Outer validity first checks the intrinsic constituents, then uses an intrinsic excursion for its own hit and wrap conditions. A subsequent outer-valid motion may repeat that validity check and then use the intrinsic motion. Each of these is a separate stratum; none tests the updated bucket or shortlist. Invalid descriptors return failure or a zero value without relying on a motion’s promised inverse.

All rate factors multiplying these terms have logarithmic range O(d): a variable bin has |\log_2(b/a)|=O(d), while f/\pi_f is bounded. Resetting a source rate to the public stage rate does not multiply the numerical term by f/u; that ratio was a norm cost. It therefore causes neither a large numerical shift nor a new long choice field. The fixed number of bounded-factor products, coefficients and O(d) scale shifts obey Theorem 10.9.

Candidate domain and bucket sums. The descriptor pool is the concatenation of the preceding list positions and this group’s unmerged paths, with invalid slots masked. A new descriptor is a representative exactly when it is the first valid new descriptor with its key and no old valid position has that key. Old valid positions remain separate. To decide these flags, enumerate the 2^{O(d)} descriptors, keeping only the current indices, bounded flags and O(d)-bit counts. Each test uses lower validity and endpoint comparison operations. The comparisons use only those unmerged paths or the preceding prefix’s already-defined positions. In particular they never inspect the new value of the bucket being defined.

An intermediate entry is the old entry at an old representative, or the previous baseline at a new representative, plus the sum of all valid matching increments in each channel. That sum has a fixed O(d)-bit descriptor domain and boundedly many 2^{O(d)} scale factors. It is evaluated by the balanced sum construction of Theorem 10.9, with the preceding domain tests as structural leaves. No high-precision sequential accumulator is held while requesting term digits. The bucket rule preserves distinct actual representatives, including when two old representatives have the same key. Thus it gives exactly the intermediate array used in Lemma 9.5.

Ranks, compression, and list selection. The intermediate domain and its values are now earlier inputs. Add enough copies of the default for the size and first-signal ranks. A finite domain of 2^{O(d)} indices suffices: the preceding list has size 2^{O(2d)} and the new group has 2^{O(d)} descriptors. The default is included as often as needed to represent the unlimited padding in the prescribed ranks. The rank, max, min, absolute-value and clipping operations of Lemma 8.1 are the finite arithmetic primitives. The ranges are 2^{O(d)} by Lemma 8.6; their known normalizing shifts have magnitude O(d).

Here u_0\ge\rho_d=2^{-c_1d}. A canonical finite approximation can test a threshold strictly between u_0 and 2u_0: with error a sufficiently small fixed fraction of \rho_d, accept every size greater than 2u_0 and accept only sizes greater than u_0. The required numerical clock, after normalizing the range, is O(d). Fix this clock and tie convention once for that structural test. Consequently every nondefault compressed position is included, and fewer than n_d positions are selected, as in Lemma 8.1. Numerical equalities at the boundary need not be decided. No default can expose a positive row score: its rank dummies close the gate first, by the margins of Lemma 5.5.

Remap a requested list ordinal to its selected intermediate descriptor by enumerating the pool and counting the preceding accepted flags. The loop stores O(d)-bit indices and a count. Its only calls are the already-defined intermediate flags and finite-margin selection tests. Compressed entry digits then query that descriptor’s intermediate value and the common compression thresholds; baseline digits use those thresholds directly. A terminal list motion selects its descriptor before delegating to an old prefix path or a new valid path. A descriptor from many prefixes ago is therefore represented by a chain of delegations, not retained as one long word above a tight child.

Presence before value or motion. Ordinal lookup returns a presence bit and a selected descriptor only when its finite enumeration reaches the requested ordinal. It starts with a false presence bit and returns false if enumeration ends first; the false branch supplies no descriptor. Every compressed-entry digit query and list motion branches on this fresh result before using a descriptor. The preceding-prefix lookup has the same convention. A hole denotes no real representative. Rank operands retain their prescribed structural selection of an entry, baseline, or padding value; they do not infer that value from the zero stream exported at an absent real port.

The final precursor A and auxiliary class A_I use the bounded final list-position alphabet, allowing holes. Their presence tests use list presence, role-membership masks, and the fixed-precision raw-entry and raw-rank tests of Lemma 5.5. Source membership is checked locally; endpoint membership uses the earlier list or intrinsic excursion with a pure membership action. It does not use the exposed-class motion whose validity is being defined. These tests precede the pre-incoming score formula and use neither its incoming gate nor its cap. Every pre-score digit invocation repeats the corresponding class test and returns zero on failure. Other uncapped row-value queries use their support-covering class in the same way. Each such class contains the entire nonzero support, so the extension agrees with the mathematical table. Existence predicates evaluate their earlier masks directly; they do not ask for their own existence. Analytical witness functions without an exported port interface retain their stated full-array values and are not restricted by this convention.

Immediate-path values and visits first use their earlier constituent and, where appropriate, outer-validity tests. Endpoint comparisons likewise test their two earlier descriptors before making visits. A capped correction-value query stops with zero if its forward paired move fails; only a successful move permits a gate or column-value query at the endpoint. The paired inverse keeps its target-side validator from Lemma 11.6. Incoming ranks and vector queries return zero outside their prescribed vertex type or membership domain. These checks are repeated at canonical entry, including when the caller is a synthetic post-initiation state with a fabricated validity flag. An excursion checks before constructing its spine; its endpoint action and rollback retain the order of Lemma 11.8.

Place these entry wrappers a fixed number of strata above their validity predicates and value or motion cores. A wrapper at clock t calls its structural test at clock zero and retains O(d) descriptor and control bits; its boundary is therefore bounded by O(d)+bt. When it subsequently calls a numerical core at clock j, the test has finished and only bounded status and descriptor data remain, so the bound ad+b(t-j) persists after enlarging a. The predicates use the fixed structural precisions already proved. They do not call the score, gate, cap, new bucket or new shortlist whose value is being checked. The finite stratum list is enlarged before choosing the allowance constants. Recipe guards permit opaque calls only to total entry wrappers, so a synthetic state cannot select a continuation that skips validation. No semantic predicate is evaluated by a guard itself.

These wrappers preserve the represented relations, values and outgoing endpoints. Their insertion may change the contour ordering of incoming ports; both directions use the same updated graph, so pairing remains consistent. The tests use the same effective tuples and fixed structural clocks, and restore the catalyst on both outcomes. They require no accuracy promise and add no retained endpoint address.

Finite strata within a group. For clarity, a permissible ordering, from an exported operation down to its dependencies, is:

1. 1.

   compressed entries, baseline and list-port operations;

2. 2.

   ordinal remapping, compression and exception selection;

3. 3.

   size and first-signal ranks of intermediate entries;

4. 4.

   intermediate domain flags and entry or bucket-sum values;

5. 5.

   first-representative and key-match predicates;

6. 6.

   endpoint comparisons of outer-valid paths;

7. 7.

   outer-valid visits, then outer path validity;

8. 8.

   intrinsic visits, constituent tests, factor digits and ordered motions, subdivided according to the preceding distinction.

The wording of an interface name does not force a call at the same stratum. For example, the “visit” used to verify outer validity is the intrinsic visit, while the visit used by key comparison is an outer-valid visit. Arrange these finite subtypes in their indicated dependency order: outer-valid visits use outer validity; outer validity uses intrinsic visits; key comparisons use outer-valid visits; and bucket predicates use those comparisons. Arithmetic on intermediate values uses only their domain flags and lower matching predicates. This refines the displayed list to a finite acyclic list. Repeated enumeration over descriptors stays in a loop of its layer, rather than creating one recursive frame per descriptor. Between these layers Theorem 10.9 gives (11.5); structural loops add O(d) bits. All remaining path calls go to the preceding prefix or to the lower-budget factors already described.

Final row classes and pre-incoming values. At the final slack d=1, the list size, port alphabet and all threshold gaps are constants. The classes and witnesses in Lemma 5.6 are defined by canonical finite-margin entry and rank tests on the final raw arrays. They can be enumerated without testing positivity of a computed score. Their tests and pre-incoming score digits query only the final buffer and a fixed arithmetic recipe. The same raw-array tuple is used for every row. A normalized dense entry uses its second raw argument, divided by the fixed scaling constant and clipped before the reciprocal. It does not start a new preparation experiment at its unbalanced endpoint.

The broader auxiliary class used to score an incoming gate depends only on the corresponding pre-incoming row calculation. Its validity and score queries do not depend on that incoming gate or cap. The precursor A for a correction has the same property. Its canonical terminal program begins with a restoring check of the full precursor class and membership domain, and sends every invalid initiation to failure. Thus Lemma 11.6 counts exactly its valid entries, not merely entries promised valid by an external caller. The auxiliary scoring program has the same initial check. Its score digits are pre-incoming, so Lemma 11.7 invokes only lower forward operations. By Lemma 5.6, discarding a precursor with more than K_c incoming entries preserves its value.

Final incoming and vector wrappers. Place the capped-pair and inverse-score wrappers above their respective terminal programs, and those programs above their pre-class, selection and pre-score queries. They are separate terminal programs: the gate score program does not call this task’s cap pairing, and the cap program does not call its gate rank. A final correction-value query first completes the paired move. At the endpoint its motion-return data consist only of the bounded inverse port while it queries a gate-rank digit or a lower-budget column-vector digit, and then returns. This can be done separately for every arithmetic operand bit. Only numerical path bits and immediate descriptors coexist with a late query. The factor r_i at a projected source is handled in the same way at that source.

A detector trial is an inverse-score wrapper of its lower-budget input row task. Reward terms query source factors locally and cross paired corrections before midpoint vector queries. Vector prefix sums use the simpler balanced arithmetic form of the same dyadic schedule. These are all the vector and incoming uses in the additive formulas. There are only a fixed number of final wrapper types. Their short counts and return ports cost a fixed allowance gap. In an inverse score program the saved numerical suffix satisfies the clock bound in Lemma 11.7; its full word is held only over structural motion. The cap wrapper’s counts have fixed size.

Uniform generation and record bounds. Each enumerated object above has a literal O(d)-bit index or is a Boolean path in one of the stated arithmetic recipes. Uniform index-generation uses finite integer loops on these indices, including rank comparison pairs and balanced-tree nodes. Constants, field/rate coefficients and walk probabilities have O(B)-bit rational descriptions. Their requested digits use integer arithmetic in scratch and make no recursive graph call. In particular, a walk word has length O(d) and a fixed rational generator probability, so its probability denominator has O(d) bits. Rate and field expressions involve fixed powers of O(B)-bit integers. The arithmetic theorem’s uniformity and public-coefficient hypotheses are thus satisfied.

The finite arithmetic list covers the formulas used here explicitly. A fixed polynomial switch is evaluated on an affine-rescaled clipped argument; positive parts and absolute values use maxima, and a variable clip is a minimum followed by a maximum. The normalizing reciprocals have their arguments clipped to [1/2,1]. The eighth roots used in the error estimates express regularity of the row functions and are not additional numerical operations requested by the controller. Ranks inside a prefix use the finite descriptor construction above; the unbounded incoming classes use Lemma 11.7. This accounts for the arithmetic primitives without adding a real-number comparison or an incoming-rank oracle.

Structural selection words and loop counters have O(d) bits. The only longer local numerical words are the early operand records of Theorem 10.9 and the just-described score suffix; they obey their explicit clock-decrement bounds. Late operand calls hold only numerical paths, pending bounded results, immediate descriptors and short inverse tokens. A fixed number of arithmetic and structural layers enlarges the constants in (11.5); its clock differences add. Ordered terminal delegations add their own immediate records, with the same estimate at each boundary, including on rollback as proved in Lemma 11.8. This verifies the record certificate on the designated executions, independently of any graph guards.□

Proof. Start with the fixed top parameters and scan the active records. An estimator edge specifies a task type, a stage change prescribed by the formula, a budget offset, a bin-scale offset if present, a bounded copy choice and channel-role recipe. These determine the next absolute stage, rates and suffixes. A projection appends the stored symbol before the inherited suffix. A fresh midpoint or vector role uses the specified public stage rate and its prescribed suffix; it does not carry the old source. These are the common-tuple recipes in Lemma 5.6 and Lemma 7.5.

An averaging edge also carries its generator and wrap word. Apply these fixed transformations in order to the current environment. Their descriptors are independent of the indicated endpoint; membership and wrap consistency are tested separately on visits to that vertex. Thus no discarded conditioning address is needed to regenerate the environment. For an old-prefix edge the tuple stays that of the same row calculation. At final assembly a gate or column multiplier uses this common tuple, rather than the internal variant which happened to lead to a selected representative. An action-owner tag allows an endpoint-local calculation to replay just to that ancestor tuple.

Numerical paths specify arithmetic operands, gates, digit places and the early-prefix modes of a reciprocal. Their finite index rules are those of Theorem 10.9; an absolute place is recovered from the root clock and the path or offset, not saved afresh per frame. Descriptor selections which used the cursor were stored explicitly as their bounded choices before movement. No later tuple computation needs to repeat such a selection at an unknown old cursor.

At every step the tuple and the temporary integers have O(B) bits in the actual parameter and clock ranges. Keep a current tuple in scratch and overwrite it as each record is processed. Repeating the scan reconstructs an ancestor or a selected candidate chain. Delimiters and marked active-copy tags specify which chain is used. This costs one scratch facility, including its scanning counters, rather than one absolute pointer, input-head position or tuple per frame.

A pure endpoint action belongs to its outer invoking predicate and may read that owner’s permitted salt. It is excluded from the lower program graph and cannot affect the lower path or rollback. Nested lower queries still restore their arbitrary incoming catalyst contents.

Finally, the only salt read by a new group comparison is its task’s own block salt. Descendants do not increase their budget. Walks alter only the already designated earlier free salt blocks and leave the present and later ones frozen. All descriptor and instruction orders are fixed index orders; all range and length checks depend only on public bounds and accessible tuple fields. Give each recipe the syntactic permission to address only those salt blocks at most its budget block in its effective environment. This is a direct range check on a requested salt index, not a condition on the salt’s value. A synthetic record cannot change that permission, choose a higher-budget recipe, or bypass the fixed parent-to-child rules. The same replay and checks are used before predecessor queries. Consequently the entire lower-block structure is independent of later salts. The clean calculation in Lemma 9.2 uses the same fixed descriptor orders and structural clocks, with its stipulated replacements of comparison predicates. The error proof uses the salt independence of the actual lower algorithms and of the clean recipes.□

Proof of Theorem 11.1. Let S exceed the finite number of operation strata in Lemma 11.10, including the subdivision of path validation and all final wrappers. Choose fixed integers K_0>S+1 and K_1>2(K_0+S+1), increasing them as needed for the local constants. Assign to an operation at budget M, prefix slack d and stratum s_0\in\{0,\ldots,S\} the allowance

Final wrappers use d=1, with increasing s_0 down their dependencies. For a nontrivial prefix, 1\le d\le M; trivial tasks use fixed top strata and terminate locally.

A same-slack descent lowers w by at least d. A preceding-prefix descent to 2d, even with a reset to an earlier stratum, lowers it by at least (K_0-S)d>d. A statistical descent to m\le M-d lowers it by at least (K_1-K_0-S)d, since the child allowance is at most K_1(1+m) minus a nonnegative stratum term. Hence every required boundary has w-w'\ge c d for a fixed c>0, and all allowances remain positive and O(1+M). The estimates (11.5) and the ordered-path record certificates give Definition 11.3, with common coefficients. When a common clock coefficient is increased, compensate the allowance coefficient using the bounded clock overshoot, just as in (11.3). Add a fixed allowance gap for a traversal wrapper’s bounded incidence, count and status data.

There are two distinct estimates in this induction. First, Lemma 11.10 certifies the raw caller words with the same a_0,b_0 at every budget; a lower opaque operation contributes its call recipe, but none of its internal working states, to that certificate. Second, Lemma 11.4 converts a copied raw portion to its physical bound with one fixed pair A,D. The induction below appends a lower operation’s physical portion; it never substitutes that physical portion into an upper raw graph state. The raw certificate therefore does not depend recursively on the already enlarged physical constants.

Construct the procedures in increasing allowance. The induction covers all recipe instances admitted by the finite range and parent-to-child checks: both designated calls and calls made when probing candidate predecessor records. It does not require such a candidate record to have occurred on a designated execution. Each opaque call still enters the lower procedure at its canonical entry, where its semantic presence tests are performed. At the bottom are local base ports, rank and salt evaluation, rational arithmetic without graph operands, and trivial zero tasks. Suppose lower operations are total, have their claimed cursor and catalyst behavior, and obey the local bounds. The finite restoring and numerical recipes of Lemma 11.10, using Theorem 10.9, then compute exactly their specified bit or digit. Their finite loops and lower calls terminate. Endpoint visits use Lemma 11.8, and completed endpoint comparisons use Lemma 11.9. The latter restores arbitrary catalyst contents and has an independent answer, preserving the induction hypothesis. The other recipes make no direct catalyst-dependent choice.

The canonical terminal programs have finite loops and only lower terminal delegations or opaque calls, so their prescribed executions terminate. Their class checks send invalid canonical initiations to failure. The certificates already proved show that all their designated boundaries fit the local bounds. By Lemma 11.11, their parameters and static guards are uniform and independent of a discarded cursor. We may therefore apply Lemma 11.4. Guards remove no designated execution. At synthetic states they ensure that every probed query has an admissible lower tuple and available space; fresh safe lower queries do not rely on the truth of an earlier stored flag.

The finite graph contours of Lemma 11.5 now implement the higher cap and inverse-rank wrappers in Lemmas 11.6 and 11.7. They terminate on success-root components even if other graph components contain cycles or guard-created dead ends. They count only the canonical initial executions of these programs, so their paired maps and ranks are the mathematical ones specified by the tables. By the common root tuple and salt convention the same maps are obtained in either direction and on every re-query. This completes the well-founded construction. An opaque query in this induction denotes its already constructed finite procedure; recursively substituting these procedures gives an ordinary deterministic machine.

The allowance is a runtime parameter of this fixed finite collection of instruction types, rather than an index for input-dependent program text. Operation tags select the finite recipe family; loop counters, gate paths and regenerable descriptors select its current instance. Thus the induction constructs one uniform interpreter for these instructions. It requires neither a separately compiled machine for each budget nor stored transition graphs for the contours.

It remains to add all simultaneously live data. By Lemma 11.4, a traversal root at (w_i,t_i) with a pending query at (w_{i+1},t_{i+1}) contributes at most

local bits, including its fixed number of neighbor-state copies. Ordinary restoring and numerical calls have the same bound after one enlargement of A,D. Inverse traversal copies only its local explicit chain, not older stack segments or the internal configurations of a transition query. Choose A,D also to dominate the bottom operation’s intrinsic linear bound. If the active chain has boundaries 0,\ldots,r, with boundary zero at the top, put \Phi_i=\Phi(w_i,t_i). The total local space is at most

Figure 1 shows which records enter each summand.

The clock inequality in (11.1) gives

Since t_i\le\Psi(w_i,t_i), all clocks are O(t_{\mathrm{top}}+w_{\mathrm{top}}). This also bounds the public scratch calculations in the arithmetic theorem. An uncharged full coefficient or cursor copy cannot persist there: any operand-dependent early word crossing a query was included in its record certificate, while pure public computations have no recursive query. The master environment, cursor, catalyst, scratch and their global scan counters are single facilities. Their total space is O(B+t_{\mathrm{top}}+w_{\mathrm{top}}).

For exact-stream semantics the induction is valid for each finite requested clock, allowing scratch to scale with that clock. Every structural domain uses its fixed finite-margin clock, so its definition does not change in this argument. In particular the integer N_t of a score rank or arithmetic operation is always evaluated by its own place convention, even when used in a request for the next digit. The actual application has M_{\mathrm{top}},t_{\mathrm{top}}=O(B), and hence all these facilities and active records use O(B) bits.□

Proof. Keep only the nonnegative summand at z. Since \Pr[X_f(z)=1]=\pi_f>0,

Dividing by \pi_f/f proves Equation (12.2). In particular, choosing one specified coordinate costs the factor N from the integrated norm. Markov’s inequality gives Equation (12.3).□

Proof of Theorem 12.1. Apply Lemma 2.1 to \mathcal M, with no promise on its acceptance probability. Set

where |V_0|\le2^{C_0B} is an explicit configuration bound. Since d is fixed, r,L=O(B). Let z be the all-primary copy of the start at stage L. Proposition 4.7 gives

This bound holds for every acceptance probability. Choose a fixed C_N large enough to bound all the resulting stage domains by N=2^{C_NB}.

For the final reward task take a=u=f=b_L. Its rank satisfies i_*=O(L+1), and Equation (7.8) reads

By Lemma 3.1, fix an integer C_{\rm tail}\ge1 bounding (f/\pi_f)C_b^8 throughout the admissible range. Choose the fixed linear coefficient of M_{\rm top}=O(B) large enough that

The top-budget and field-size choices in the preceding subsection allow this enlargement; Equation (12.1) still bounds every descendant rate. Theorem 9.8 supplies the reward moment estimate. Lemma 12.2, with \eta=\Delta/8, now shows that

Thus the factor N lost on selecting one coordinate has been paid by the statistical precision. Explicitly, the bound in Equation (12.3) is at most

by Equation (12.5).

We next turn the estimator values into a finite list of dyadic numbers. For each master environment, Theorem 10.9 gives the digits w_j\in\{-6,\ldots,6\} of its one fixed value \bar W_L(z). Structural choices do not depend on the requested digit. Put K=r+6, compute

The integer A_\sigma is obtained by starting at zero and applying A\leftarrow2A+w_j in order, so it uses O(K) bits. By Equation (10.2), the truncation error is at most 6\,2^{-K}<\Delta/8. Clipping cannot increase error relative to W_L(z)\in[0,1]. Equations (12.4) and (12.6) imply that, on more than three quarters of the environments conditioned on X_f(z)=1,

Enumerate the conditional law exactly. Enumerate each field-matrix entry in \{0,\ldots,P-1\} and each raw salt bit string, retaining precisely those encodings whose positive-degree columns form a frame and for which X_f(z)=1. The retained encodings are equally weighted and give the law in Equation (12.6). In particular, enumerate the original salt strings, not their reduced fingerprint parameters. Different raw strings that induce the same fingerprint remain separate encodings; their multiplicities reproduce the original probability law. At least one encoding is retained: a frame exists, and its independent constant column can place the designated evaluation in the nonempty retention box. The matrices have fixed dimensions and \log P=O(B); together with Equation (9.4), this gives O(B) bits per master environment and at most 2^{O(B)} encodings to enumerate.

Let E\ge1 be the number of retained encodings, found by one pass, and let h=\lfloor E/2\rfloor+1. Binary-search the integer interval [0,2^K] for the least a such that at least h retained encodings satisfy a_\sigma\le a. Each count is computed by a fresh pass, recomputing each numerator a_\sigma. This finds the upper median of the finite multiset, including all repetitions. Since more than three quarters of its members satisfy Equation (12.7), so does its median: fewer than E/4 values can lie below the indicated interval, and fewer than E/4 can lie above it. The algorithm retains only the current count and search registers; it never stores the multiset. Output the integers (a,K) representing z_x=a2^{-K}. Then

We account for the memory held during this computation. The master environment, current cursor, catalyst, shared scratch, and suspended controller records together use O(B) bits by Theorem 11.1, because M_{\rm top},K=O(B). The outer computation keeps only a fixed number of additional O(B)-bit registers: its top parameters and designated start, the environment enumeration index, E, h, the current count, the two binary-search endpoints and candidate, the digit index, and the signed numerator accumulator. Each count is bounded by the number of environment encodings, so it also has O(B) bits. These outer registers remain live while a digit query runs; in particular, both its environment-enumeration state and its numerator accumulator are included. They are present once for the whole computation, not once per recursive level. Every query terminates on every environment, including the inaccurate environments, by the same realization theorem. The output is written only after the median is computed.

Each digit query is a halting deterministic computation with O(B) work bits and physical input heads confined between the real endmarkers. Counting its finite control, work-tape contents, and all work and input head positions gives at most 2^{O(B)} complete configurations on its fixed input. A repeated complete configuration would force a deterministic loop, so totality bounds the query by 2^{O(B)} steps. There are 2^{O(B)} environment encodings, O(K+1) binary-search passes, and K+1 digit queries per numerator. Their product is still 2^{O(B)}=(n+2)^{O(1)}. All finite parameters are generated uniformly, and all constants are fixed for (\mathcal M,d).□

Proof of Theorem 1.1. Let \mathcal M recognize a language in \BPL, with acceptance probability at most 1/3 on no inputs and at least 2/3 on yes inputs. Apply Theorem 12.1 with d=3. For every input length, including n=0, its error is at most (n+2)^{-3}\le1/8. Hence the dyadic answer is at most 1/3+1/8=11/24 on a no input and at least 2/3-1/8=13/24 on a yes input. Comparing this answer with 1/2 decides the language uniformly in logarithmic space. This proves \BPL\subseteq\Lclass directly from probability approximation.

A deterministic machine may ignore its coins, giving \Lclass\subseteq\RL. Two independent repetitions of an \RL machine, accepting if either repetition accepts, have acceptance probability zero on no inputs and at least 3/4 on yes inputs. They use logarithmic space and polynomial time, so \RL\subseteq\BPL. The three inclusions prove \Lclass=\RL=\BPL.□

Proof. The same d=3 approximation and threshold 1/2 used in the preceding proof accept every input in Y and reject every input in N. The resulting machine halts also outside the promise because its approximation queries are total. The reverse inclusion follows by ignoring the coins.□

Proof of Theorem 1.2. Fix a padded machine \mathcal M_{\rm pad} as follows. On a string beginning with 1^n0x, where |x|=n, it simulates \mathcal M(x) and ignores all remaining symbols. If the delimiter or the following n symbols are absent, it rejects. This is one fixed randomized machine with polynomial worst-case running time and logarithmic work space in its full input length. On every string with the specified prefix its acceptance probability is p_{\mathcal M}(x). Fix once and for all the transducer of Theorem 12.1 for \mathcal M_{\rm pad} and d=1.

On input (x,1^q), with n=|x| and q\ge1, set

Simulate that fixed transducer on the virtual length-m string

An input query is answered by comparing its address with the prefix boundaries and either returning the appropriate bit of x or a fixed bit. The simulated input-head address and all these comparisons use O(\log m) bits; the string y is never stored. The simulated transducer returns a dyadic rational z\in[0,1] satisfying

Its numerator and exponent have O(\log m) bits and can be retained in work space while its finite output is simulated.

Compute by exact dyadic arithmetic

Then 0\le a\le2^{q+2}, and rounding gives

Write the binary numerator a to the output tape. It has at most q+3 bits and represents the denominator specified in the theorem. The simulator state, virtual input address, actual input counters, captured dyadic answer, and rounding operands occupy a fixed number of records of total size

The simulation and the synthesis of each input bit take polynomial time in m, so the total time is m^{O(1)}=(n+2)^{O(1)}2^{O(q)}. The padded machine and its exponent-one approximator were fixed before reading q. Thus their constants are independent of the requested accuracy. Throughout their simulation, the original size convention is B=\Theta(\log(m+2)), exactly as required by the estimator and controller theorems.□

Proof. Give halted configurations constant self-transitions through time T(n). A configuration and its elapsed time use O(\log(n+2)) bits. There is a fixed randomized logarithmic-space continuation machine which, on a valid encoding of (x,v,t), starts from configuration v and simulates the remaining T(n)-t steps with fresh coins. It checks the fixed work-space box and time bound, rejecting malformed encodings and any attempted violation. Its acceptance probability on the reachable configurations is the continuation value p_t(v), and it has a polynomial worst-case time bound in its input length.

Write \gamma=(n+2)^{-c}. Choose a fixed exponent d large enough that Theorem 12.1, applied to the continuation machine, approximates every queried value within \delta\le\gamma/(8T(n)). Such a fixed exponent exists because T is a fixed polynomial and the continuation input contains x. The extra fields have logarithmic length. We supply them virtually from saved configuration and time registers, so the approximation and those registers together use logarithmic space.

Starting at the initial configuration, at each time estimate the continuation value of every positive-probability successor and choose one with maximum estimated value, breaking ties by a fixed port order. Since p_t(v) is the weighted mean of the successor values, the chosen successor v' satisfies

On an input satisfying the stated lower bound, after T(n) choices the terminal continuation value is at least \gamma-2T(n)\delta\ge3\gamma/4>0. A terminal continuation value is zero or one, so this computation accepts.

First run this construction without writing output. If its terminal state rejects, output the failure symbol. Otherwise repeat the same deterministic choices and stream the configurations through the original first halting state, or the symbols emitted by the simulated transducer. The artificial self-transitions after halting are omitted from the output. This second pass follows the same accepting computation. Consequently no rejecting computation is output, even outside the probability promise.

At any time the current, candidate, and best successor configurations, the time counter, a constant number of dyadic scores, the virtual input address, and the approximation workspace occupy a constant number of O(\log(n+2))-bit records. The finite successor lists have constant size, and there are only T(n) steps in each pass, so the total running time is polynomial. Each approximation has a deterministic guarantee at its queried configuration; no simultaneous accuracy event for all adaptive queries is needed.□

Proof. Count m before interpreting the prefix. Scan the unary code-length header with a bounded counter, rejecting if its length exceeds \lambda_m or the required delimiter is absent. Check the two eligibility conditions before copying z or allocating simulation storage. Then verify that the following d_{\mathrm{code}} code bits, the unary data-length header, and the required data bits are present. The parsed n is at most m, and d_{\mathrm{code}}n\le\lambda_m m, so even size calculations preceding a failed length check use only O(\lambda_m) bits. List counts, ID lengths, tape declarations, and movements are checked against the actual code and the stated bounds before any loops or allocations using them. There is no enumeration of an implicit domain of symbol or state names.

Store the encoded tapes sequentially on a fixed number of real work tapes of U. At most d_{\mathrm{code}} strips, each with 2R+1 cells of d_{\mathrm{code}} bits, require

bits. Indeed, eligibility gives d_{\mathrm{code}}^3\le\lambda_m and d_{\mathrm{code}}^2R\le\lambda_m. The copied program, current state, scanned and written symbol tuples, coin block, strip coordinates, step counter, and parsing scratch fit simultaneously in O(\lambda_m) bits. A single simulated input-head coordinate has magnitude O(m) by the transition cap and therefore also uses O(\lambda_m) bits. Read the corresponding source symbol by rescanning the encoded data, supplying the appropriate markers or off-data blanks according to the encoded input-tape convention.

All routines are bounded scans and ordinary binary arithmetic. They iterate over actual code positions, input positions, a bounded tape/head list, strip positions, and bit positions, with a fixed nesting depth. Each range is polynomially bounded in m+2; binary arithmetic is implemented by bit scans, not unit-cost operations on growing words. Matching a listed transition, fetching input symbols, updating the strips, and obtaining its finite coin block therefore take polynomial time in m+2, with one fixed exponent determined by these routines. The same bounds hold when a check fails. There are at most m interpreted transitions. Checking the initial halting state and the state reached by the last permitted transition gives the asserted total behavior, including m=0. The resulting fixed U has the required polynomial worst-case time on every random tape.□

Completion of the proof of Theorem 13.1. The compiler returns the described machine D and the integers K,H,c in Equation (13.11). Its finite syntactic construction terminates. On every promised source input, Equation (13.9) and the fixed separator’s threshold guarantee give the correct decision. The totality of A and the finite callback loops prove halting. Equations (13.12) and (13.14) give at most K\log_2(n+2) work bits and H(n+2)^c bit operations for this same machine.

All claims include n=0: then B_n=1, the real-input scans are empty, the count n+1=1 has one bit, and every displayed padding, strip, space, and time inequality remains valid. The library’s grouping width already includes its finitely many small-length exceptions. All construction constants are fixed before the ordinary input is read.

The work and time internal to probability approximation—environment enumeration, numerical digits, recursive interfaces, recomputation, and precision management—belong to the one complete library machine proved in Theorem 12.1. Its tapes remain counted throughout virtualization. The compiler adds only the exact input operations analyzed here, without an evaluation oracle or an external stack. Configuration counting gives polynomial time because this entire deterministic machine uses exact logarithmic space.□