3 Encodings and finite probability
This chapter covers the machine-independent layer that every other chapter relies on: how objects become binary strings, and how probabilities over random bit strings are counted. Formalized so far: fixed-length bit strings and their bridge to lists; the self-delimiting block framing and the pairing function \(\langle x, y \rangle \), the library’s standard way to hand a machine two strings, with polynomial-time projections; canonical binary natural numbers; a rose-tree serialization; row-major adjacency matrices; a canonical code for fan-in-two circuits; exact counting over \(\{ 0,1\} ^T\); uniform event probability with the union bound, Markov’s inequality, and majority amplification with explicit constants; and a fixed-time repetition wrapper for probabilistic machines whose acceptance probability is exactly a majority-event probability. The main open direction is consolidation: about 24 modules define ad hoc codecs and about 25 define ad hoc probability notions, which a reusable codec interface (Definition 65) and Mathlib’s Finset.expect and Finset.dens should absorb.
3.1 Bit strings
A bit string of length \(n\) is a function \(\{ 0, \dots , n-1\} \to \{ 0,1\} \). Circuits consume bit strings of a fixed length; machines consume lists.
\(\mathrm{toList}(x) = [x_0, \dots , x_{n-1}]\) serializes in increasing index order; \(\mathrm{ofList}\) reads a list whose length is proved to be \(n\); and \(\mathrm{toTotal}(x) : \mathbb {N} \to \{ 0,1\} \) extends \(x\) by \(0\) outside its range. The variable-length correspondence \(\{ 0,1\} ^* \simeq \Sigma _n \{ 0,1\} ^n\) is Mathlib’s.
\(|\mathrm{toList}(x)| = n\) and the \(i\)-th entry of \(\mathrm{toList}(x)\) is \(x_i\); \(\mathrm{toList}(\mathrm{ofList}(\ell )) = \ell \) and \(\mathrm{ofList}(\mathrm{toList}(x)) = x\); \(\mathrm{toList}\) is injective; and \(\mathrm{toList}\) sends concatenation of bit strings to list append.
Mathlib’s List.ofFn lemmas.
3.2 Self-delimiting blocks and pairing
The block of \(x = x_1 \cdots x_n\) is \(\mathrm{delimit}(x) = x_1 x_1\, x_2 x_2 \cdots x_n x_n\, 0 1\): every bit is doubled and the separator \(01\) ends the block. The parser \(\mathrm{unpair?}\) reads one block off the front of a string and returns the payload and the remaining suffix, or fails on malformed input; \(\mathrm{undelimitBlocks}\) parses a string that consists entirely of blocks into the list of their payloads, or fails. The total helpers used by machines are: \(\mathrm{undelimitBlock}\), the payload of the leading block (empty on malformed input); \(\mathrm{takeFirstBlock}\), the leading block itself, framing included (empty on malformed input); \(\mathrm{hasBlock}\), whether the string begins with a well-formed block; and \(\mathrm{tagBlock}(z)\), which is \(1z\) if \(\mathrm{hasBlock}(z)\) and the empty string otherwise.
\(|\mathrm{delimit}(x)| = 2|x| + 2\). For all \(x, y\), \(\mathrm{unpair?}(\mathrm{delimit}(x)\, y) = (x, y)\), and conversely if \(\mathrm{unpair?}(z) = (x, y)\) then \(z = \mathrm{delimit}(x)\, y\). For every list of strings \(b_1, \dots , b_m\), \(\mathrm{undelimitBlocks}(\mathrm{delimit}(b_1) \cdots \mathrm{delimit}(b_m)) = [b_1, \dots , b_m]\). Finally \(\mathrm{undelimitBlock}(\mathrm{delimit}(x)\, y) = x\), \(\mathrm{takeFirstBlock}(\mathrm{delimit}(x)\, y) = \mathrm{delimit}(x)\), and \(\mathrm{hasBlock}(z)\) holds exactly when \(\mathrm{unpair?}(z)\) succeeds.
Induction on the payload; no doubled pair equals the separator.
\(\langle x, y \rangle = \mathrm{delimit}(x)\, y\): the first component is framed as a block and the second is appended verbatim.
\(|\langle x, y \rangle | = 2|x| + 2 + |y|\). Indexing from \(0\), with \(x = x_0 \cdots x_{|x|-1}\) and \(y = y_0 \cdots y_{|y|-1}\): bits \(2i\) and \(2i + 1\) of \(\langle x, y \rangle \) are \(x_i\) for \(i {\lt} |x|\), bits \(2|x|\) and \(2|x| + 1\) are \(0\) and \(1\), and bit \(2|x| + 2 + j\) is \(y_j\) for \(j {\lt} |y|\).
Induction on \(x\); the positions in \(y\) by splitting the concatenation.
If \(\langle x_1, y_1 \rangle = \langle x_2, y_2 \rangle \) then \(x_1 = x_2\) and \(y_1 = y_2\). Moreover \(\mathrm{unpair?}(z) = (x, y)\) if and only if \(z = \langle x, y \rangle \).
Injectivity by induction on \(x_1\), comparing a doubled pair with the separator. The decoding characterization is the block round trip of Lemma 51.
\(\pi _1\) reads doubled bits until the separator (returning the bits read so far on malformed input), and \(\pi _2\) returns the suffix after the first block, or the empty string if there is no valid block. Both are total.
\(\pi _1 \langle x, y \rangle = x\), \(\pi _2 \langle x, y \rangle = y\), and \(|\pi _2(z)| \le |z|\) for every \(z\).
The first identity by induction on \(x\); the second is the block round trip. For the length bound, either \(\pi _2(z)\) is empty or a successful parse writes \(z = \langle x, \pi _2(z) \rangle \).
\(\pi _1, \pi _2 \in \mathsf{FP}\), and if \(a, b \in \mathsf{FP}\) then \(z \mapsto \langle a(z), b(z) \rangle \in \mathsf{FP}\); in particular \(z \mapsto \langle f(z), z \rangle \in \mathsf{FP}\) for every \(f \in \mathsf{FP}\). Concretely, if a deterministic machine computes \(f\) in time \(T\), a derived machine computes \(z \mapsto \langle f(z), z \rangle \) in time \(5T(n) + n + 12\). Consequently, for every \(L \in \mathsf{P}\), the languages \(\{ z : \pi _1(z) \in L\} \) and \(\{ z : \pi _2(z) \in L\} \) are in \(\mathsf{P}\).
The projections are computed by dedicated block-scanning machines with no work tapes, built for the Cobham development (Cobham’s theorem itself is not used). Pairing a value with the input, \(z \mapsto \langle f(z), z \rangle \), is a direct machine construction: run \(f\) with its output redirected to a work tape, rewind that tape and the input, and emit the framed value followed by a copy of the input. For general \(a, b\), compose \(z \mapsto \langle b(z), z \rangle \) with \(w \mapsto \langle a(\pi _2(w)), w \rangle \) to obtain \(z \mapsto \langle a(z), \langle b(z), z \rangle \rangle \), then apply a polynomial-time machine sending \(\langle u, \langle v, z \rangle \rangle \) to \(\langle u, v \rangle \). The statements about \(\mathsf{P}\) are closure under \(\mathsf{FP}\) preimages.
3.3 Other formalized codes
\(\mathrm{bin}(v)\) is the minimal binary expansion of \(v \in \mathbb {N}\), least significant bit first, with \(\mathrm{bin}(0)\) empty. The decoder accepts a string only if it is the minimal expansion of its value, so representations with trailing high zeros are rejected. The code is not prefix-free; an enclosing framing layer fixes the field boundary.
\(\mathrm{decode}(\mathrm{bin}(v)) = v\), and more precisely \(\mathrm{decode}(w) = v\) if and only if \(w = \mathrm{bin}(v)\); \(|\mathrm{bin}(v)|\) is the bit length of \(v\) (Mathlib’s Nat.size); and \(\mathrm{bin}\) is injective.
Mathlib’s Nat.bits API.
A rose tree is a finite list of rose trees; the size of a node with children \(d_1, \dots , d_m\) is \(2 + \sum _i \mathrm{size}(d_i)\). A tree is serialized as balanced brackets: \(0\) opens a node, its children follow in order, and \(1\) closes it. A stack-based parser \(\mathrm{fromBits}\) returns a tree or fails. A type with an injective map into rose trees (instances exist for rose trees themselves, Booleans, natural numbers, lists, options, and products) gets a bit-string encoding by composing with this serialization. This layer supports the rose-tree machine model.
\(\mathrm{fromBits}(\mathrm{toBits}(d)) = d\) for every rose tree \(d\); the serialization of \(d\) has length \(\mathrm{size}(d)\); the serialization is injective; and the derived bit-string encoding of any encodable type is injective.
The parser appends each serialized subtree to the top frame of its stack, by strong induction on size.
An \(n \times n\) Boolean matrix (the adjacency matrix of a directed graph on \(n\) vertices) corresponds bijectively to a bit string in \(\{ 0,1\} ^{n \cdot n}\) by row-major serialization, entry \((i, j)\) at position \(n i + j\). In particular there are exactly \(2^{n \cdot n}\) such matrices. No module of the library uses this codec yet.
A raw circuit is a list of gates, each an AND or OR of two absolute wire indices with a negation flag on each input. At arity \(N\), wires \(0, \dots , N-1\) are the inputs and gate \(i\) produces wire \(N + i\); the raw circuit is well formed if it is nonempty and gate \(i\) reads only wires below \(N + i\). A raw circuit is encoded as its gate count in terminated unary (\(m\) ones, then a zero) followed by its gates, each gate as an operation bit (\(1\) for AND), two negation bits, and its two input wire indices in terminated unary. The code \(\mathrm{code}(C)\) of a single-output circuit \(C\) over the fan-in-two AND/OR basis is the encoding of the raw circuit formed by its internal gates in order followed by its output gate. The raw evaluator computes the wires in order in a memo array and returns the last gate’s value, failing on an empty gate list or on a reference to a wire not yet computed. \(\mathrm{evalCode}(N, w, x)\) fails unless \(|x| = N\); otherwise it decodes \(w\) exactly (rejecting malformed codes and trailing bits) and runs the raw evaluator on \(x\).
The raw decoder is exact: it returns \(c\) on \(w\) if and only if \(w\) is the encoding of \(c\). The raw evaluator succeeds on \(x\) if and only if the raw circuit is well formed at arity \(|x|\). Let \(C\) be a single-output fan-in-two AND/OR circuit on \(N \ge 1\) inputs with size \(s\) (internal and output gates). For every \(x \in \{ 0,1\} ^N\), \(\mathrm{evalCode}(N, \mathrm{code}(C), \mathrm{toList}(x)) = C(x)\) (equivalently, \(\mathrm{evalCode}(N, \mathrm{code}(C), \ell ) = C(\mathrm{ofList}(\ell ))\) for every list \(\ell \) of length \(N\)), and \(|\mathrm{code}(C)| \le 1 + s(2(N + s) + 6)\).
The decoder is exact on canonical codes, and the array-backed evaluator agrees with the typed evaluation gate by gate.
3.4 A reusable codec interface
The codes above were written one at a time, and many more live inside individual proofs. The following planned nodes describe the shared interface that should replace them.
A binary codec for a type \(\alpha \) with a size measure \(\| \cdot \| \) consists of an encoder \(e : \alpha \to \{ 0,1\} ^*\), a partial decoder \(d : \{ 0,1\} ^* \to \alpha \cup \{ \bot \} \), the round trip \(d(e(a)) = a\), canonicity (\(d(w) = a\) implies \(w = e(a)\)), and an explicit size bound \(|e(a)| \le s(\| a\| )\). The existing rose-tree encodings (Definition 60) give injectivity only, with no decoder at the level of \(\alpha \) and no size bound.
From codecs for \(\alpha \) and \(\beta \), the product codec encodes \((a, b)\) as \(\langle e_\alpha (a), e_\beta (b) \rangle \), with \(|e(a, b)| = 2|e_\alpha (a)| + 2 + |e_\beta (b)|\), and the tagged-sum codec prefixes one tag bit. Both satisfy the codec laws.
For every \(n \ge 1\) there is a codec for \(\{ 0, \dots , n-1\} \) all of whose codewords have length \(\lceil \log _2 n \rceil \), whose decoder rejects values \(\ge n\). (An internal fixed-width layout, Complexity.finCodec, already has width \(\lceil \log _2 n \rceil \) and a round trip, but its decoder is total, reducing modulo \(n\), so it is neither partial nor canonical.)
From a codec for \(\alpha \), a codec for lists over \(\alpha \) that frames each element as a block, with \(|e([a_1, \dots , a_m])| = \sum _i (2|e(a_i)| + 2)\).
Canonical codecs, with explicit length bounds, for finite functions (truth tables), machine states, configurations of time-bounded runs, and bounded interaction transcripts. (Internal fixed-width layouts of machine states and of bounded configuration windows, Complexity.qCodec and Complexity.codeCodec, have exact widths but total, non-canonical decoders.)
3.5 Finite counting
\(|\{ 0,1\} ^T| = 2^T\), and \(|\{ 0,1\} ^{a+b}| = 2^a \cdot 2^b\).
Mathlib’s cardinality of function types.
\(\{ 0,1\} ^{a+b} \simeq \{ 0,1\} ^a \times \{ 0,1\} ^b\) splits a string into its length-\(a\) prefix and length-\(b\) suffix, with concatenation as the inverse, and \(\{ 0,1\} ^{kT} \simeq (\{ 0,1\} ^T)^k\) splits it into \(k\) blocks in row-major order: block \(i\) is positions \(iT, \dots , iT + T - 1\). For an event \(E \subseteq \{ 0,1\} ^T\) and \(w \in \{ 0,1\} ^{kT}\), \(\# _E(w)\) is the number of blocks of \(w\) lying in \(E\).
The number of \(w \in \{ 0,1\} ^{a+b}\) whose prefix satisfies \(P\) and whose suffix satisfies \(Q\) is \(|P| \cdot |Q|\). Exactly \(\binom {k}{r}\) vectors in \(\{ 0,1\} ^k\) have \(r\) ones. More generally, for a finite set \(\alpha \) and \(E \subseteq \alpha \), exactly \(\binom {k}{j} |E|^j (|\alpha | - |E|)^{k-j}\) tuples in \(\alpha ^k\) have exactly \(j\) entries in \(E\); for a finite set \(J\) of counts, the vectors (respectively tuples) whose number of ones (respectively entries in \(E\)) lies in \(J\) number the corresponding sum over \(j \in J\). In particular the number of \(w \in \{ 0,1\} ^{kT}\) with \(\# _E(w) = j\) is \(\binom {k}{j} |E|^j (2^T - |E|)^{k-j}\).
Transport along the block equivalences, identify a vector with its set of ones, and count tuples by the positions of their entries in \(E\).
The number of points satisfying some \(p_i\), \(i \in s\), is at most \(\sum _{i \in s} |p_i|\). Consequently, if bad sets \(B_i \subseteq S\), indexed by a finite set \(I\), satisfy \(\sum _{i \in I} |B_i| {\lt} |S|\), some \(s \in S\) lies in no \(B_i\).
Cardinality of a finite union.
For \(f \in \{ 0,1\} ^k\), \(\mathrm{maj}(f) = 1\) if and only if more than \(k/2\) positions of \(f\) are \(1\) (strict majority). For \(w \in \{ 0,1\} ^{kT}\), \(\mathrm{maj}_E(w) = 1\) if and only if \(2\, \# _E(w) {\gt} k\).
\(|\{ f : \mathrm{maj}(f) = 1\} | = \sum _{r = \lfloor k/2 \rfloor + 1}^{k} \binom {k}{r}\) and \(|\{ f : \mathrm{maj}(f) = 0\} | = \sum _{r=0}^{\lfloor k/2 \rfloor } \binom {k}{r}\). For \(2r + 1\) blocks, \(|\{ w : \mathrm{maj}_E(w) = 0\} | = \sum _{j=0}^{r} \binom {2r+1}{j} |E|^j (2^T - |E|)^{2r+1-j}\). Moreover \(\# _E(w) + \# _{E^c}(w) = k\), and when \(k\) is odd, \(\mathrm{maj}_{E^c}(w) = 1 - \mathrm{maj}_E(w)\) and negating every bit of \(f\) flips \(\mathrm{maj}(f)\).
Sum the exact fiber counts. At odd length there are no ties.
3.6 Event probability
For a finite event \(E \subseteq \{ 0,1\} ^T\), \(\Pr [E] = |E| / 2^T \in \mathbb {Q}\).
\(|E| \le 2^T\) and \(0 \le \Pr [E] \le 1\); \(E \subseteq F\) implies \(\Pr [E] \le \Pr [F]\); \(\Pr [E^c] = 1 - \Pr [E]\), and for every \(f : \{ 0,1\} ^T \to \{ 0,1\} \), \(\Pr [f = 1] = 1 - \Pr [f = 0]\); \(\Pr [\emptyset ] = 0\) and \(\Pr [\{ 0,1\} ^T] = 1\); and \(\Pr [\sigma (E)] = \Pr [E]\) for every bijection \(\sigma \) of \(\{ 0,1\} ^T\).
Cardinality arithmetic.
\(\Pr [E \cup F] \le \Pr [E] + \Pr [F]\), and \(\Pr [\bigcup _{i \in s} E_i] \le \sum _{i \in s} \Pr [E_i]\) for every finite family, with equality when the family is pairwise disjoint. If a map \(f\) sends every point of \(E\) into a finite set \(s\), then \(\Pr [E] = \sum _{i \in s} \Pr [E \cap f^{-1}(i)]\).
Induction on the index set for the union bound; the cardinality of a disjoint union for the two equalities.
Let \(w : \{ 0,1\} ^T \to \mathbb {Q}_{\ge 0}\) and \(\theta {\gt} 0\). If \(w(r) \ge \theta \) for every \(r \in E\), then \(\Pr [E] \le \mathbb {E}_r[w(r)] / \theta \), where \(\mathbb {E}_r[w(r)] = 2^{-T} \sum _r w(r)\) is the uniform average.
Compare sums.
\(\Pr _{w \in \{ 0,1\} ^{a+b}}[P(\text{prefix}) \wedge Q(\text{suffix})] = \Pr [P] \cdot \Pr [Q]\).
Divide the counting form by \(2^{a+b}\).
Let \(\pi : \{ 0,1\} ^m \to \{ 0,1\} ^c\) be a map each of whose fibers has exactly \(2^g\) elements, and let \(A \subseteq \{ 0,1\} ^m\) and \(G \subseteq \{ 0,1\} ^c\) satisfy \(w \in A \iff \pi (w) \in G\). Then \(|A| = |G| \cdot 2^g\), and if \(m = c + g\) then \(\Pr [A] = \Pr [G]\).
Sum the fiber sizes over \(G\).
With \(p = \Pr [E]\), the probability over \(w \in \{ 0,1\} ^{(2r+1)T}\) that \(\mathrm{maj}_E(w) = 0\) is \(\sum _{j=0}^{r} \binom {2r+1}{j} p^j (1-p)^{2r+1-j}\).
Normalize the exact count.
For every \(r \in \mathbb {N}\) and every rational \(p\) with \(2/3 \le p \le 1\), \(\sum _{j=0}^{r} \binom {2r+1}{j} p^j (1-p)^{2r+1-j} \le \frac13 (8/9)^r\).
For \(j \le r\), \((1-p)^{r-j} \le p^{r-j}\), so each term is at most \(\binom {2r+1}{j} p^r (1-p)^{r+1}\). The coefficients \(\binom {2r+1}{0}, \dots , \binom {2r+1}{r}\) sum to \(4^r\), and \(p(1-p) \le 2/9\) and \(1 - p \le 1/3\). This is an elementary bound, not a Chernoff bound.
Let \(E \subseteq \{ 0,1\} ^T\) and \(K = 12k + 1\), with probabilities taken over \(w \in \{ 0,1\} ^{KT}\) read as \(K\) blocks. If \(\Pr [E] \ge 2/3\), then \(\Pr [\mathrm{maj}_E(w) = 0] \le 2^{-k}\) and \(\Pr [\mathrm{maj}_E(w) = 1] \ge 1 - 2^{-k}\). If \(\Pr [E] \le 1/3\), then \(\Pr [\mathrm{maj}_E(w) = 1] \le 2^{-k}\).
With \(r = 6k\), the exact tail and the elementary bound give \(\Pr [\mathrm{maj}_E = 0] \le \frac13 (8/9)^{6k} \le 2^{-k}\), since \((8/9)^6 \le 1/2\). The second statement passes to the complementary outcome. For the third, \(\Pr [E^c] \ge 2/3\), and at an odd number of blocks \(\mathrm{maj}_E = 1\) exactly when \(\mathrm{maj}_{E^c} = 0\).
If \(\sum _{i \in I} \Pr [B_i] {\lt} 1\) for bad events \(B_i \subseteq \{ 0,1\} ^S\) indexed by a finite set \(I\), some seed lies in no \(B_i\). In particular, if \(\Pr [B_x] \le 2^{-(n+1)}\) for every \(x \in \{ 0,1\} ^n\), one seed avoids every \(B_x\).
The probabilistic method: the union bound in counting form.
The acceptance probability of \(N\) on \(x\) with clock \(T\) is the event probability of the set of accepting choice sequences in \(\{ 0,1\} ^T\), and the probability of output \(y\) is the event probability of the set of choice sequences along which \(N\) halts with output \(y\). Clocks can be extended: if every trace of length \(T\) from a configuration \(c\) ends halted and \(T \le T'\), then every decidable event on the final configuration has the same probability over traces of length \(T'\) from \(c\) as over traces of length \(T\). In particular, if every trace of \(N\) on \(x\) halts within \(T\) steps and \(T \le T'\), the acceptance probability and every output probability of \(N\) on \(x\) agree at clocks \(T\) and \(T'\); and if, on every input \(x\), every trace of \(N\) halts within \(T(|x|)\) steps and \(T \le T'\) pointwise, then for every \(x\) they agree at clocks \(T'(|x|)\) and \(T(|x|)\).
The first two statements are definitional. For clock extension, a halted trace is unchanged by further steps, so the event on a choice sequence of length \(T'\) depends only on its length-\(T\) prefix, and block independence with a trivial event on the suffix gives the equality.
\(\Pr [E]\) equals Mathlib’s density Finset.dens of \(E\) in \(\{ 0,1\} ^T\), and the uniform average in Lemma 79 is Mathlib’s Finset.expect, so the laws above follow from Mathlib’s general finite-probability API.
3.7 Repetition of probabilistic machines
For a machine \(N\) with \(n\) work tapes, \(\mathrm{rep}(N, k, T)\) has \(k(n+1)\) work tapes and performs \(k\) sequential runs of \(N\) for exactly \(T\) steps each, each run on a fresh bank of \(n + 1\) work tapes (the last simulating the output tape). Two setup transitions precede the first run. After each run it rewinds the input tape and the run’s bank in exactly \(T + 1\) transitions and records the run’s verdict in one more; after the last run it writes the strict majority of the \(k\) verdicts to its output tape (so for \(k = 0\) it writes \(0\)). Every run occupies exactly \(2T + 2\) transitions whether or not \(N\) halts early, so the total time is \(2 + k(2T + 2)\), and simulated step \(t\) of run \(j\) uses the choice bit at the fixed position \(2 + j(2T + 2) + t\). The compact seed of a choice sequence is the \(kT\) bits at those positions, and the accepting event of \(N\) on \(x\) is the set of \(r \in \{ 0,1\} ^T\) along which \(N\) on \(x\) halts with output cell \(1\) equal to \(1\).
Let \(\ell = 2 + k(2T + 2)\). Entry \(iT + t\) of the compact seed of \(r \in \{ 0,1\} ^\ell \) (\(i {\lt} k\), \(t {\lt} T\)) is \(r_{2 + i(2T+2) + t}\). Every \(s \in \{ 0,1\} ^{kT}\) is the compact seed of exactly \(2^{2 + k(T+2)}\) sequences in \(\{ 0,1\} ^\ell \), so for every predicate \(P\) on \(\{ 0,1\} ^{kT}\) the number of \(r \in \{ 0,1\} ^\ell \) whose compact seed satisfies \(P\) is \(|P| \cdot 2^{2 + k(T+2)}\), and its probability is \(\Pr [P]\). Consequently, if a machine \(M\) on input \(x\) halts with output cell \(1\) equal to \(1\) along \(r \in \{ 0,1\} ^\ell \) exactly when the compact seed of \(r\) satisfies \(P\), then the acceptance probability of \(M\) on \(x\) with clock \(\ell \) is \(\Pr _{s \in \{ 0,1\} ^{kT}}[P(s)]\).
Split off the two setup bits with the block equivalence, then split the strides into their \(kT\) simulation slots and \(k(T+2)\) administrative slots; the fiber count follows, and Lemma 81 cancels the ignored bits.
Suppose every trace of \(N\) on \(x\) has halted after \(T\) steps. Then for every choice sequence \(r\) of length \(2 + k(2T + 2)\), the trace of \(\mathrm{rep}(N, k, T)\) on \(x\) ends halted with output head at cell \(1\) and output cell \(1\) equal to \(\mathrm{maj}_E\) of the compact seed of \(r\), where \(E\) is the accepting event of \(N\) on \(x\).
Invariants for the setup, simulation, rewind, and finish phases of each stride.
Under the same hypothesis, the acceptance probability of \(\mathrm{rep}(N, k, T)\) on \(x\) with clock \(2 + k(2T + 2)\) equals \(\Pr _{s \in \{ 0,1\} ^{kT}}[\mathrm{maj}_E(s) = 1]\), where \(\Pr [E]\) is exactly the acceptance probability of \(N\) on \(x\) with clock \(T\). Without any hypothesis on \(N\), \(\mathrm{rep}(N, 0, T)\) accepts every \(x\) with probability \(0\) at clock \(2\).
By pathwise correctness, acceptance factors through the compact seed, and Lemma 89 cancels the administrative choice bits. With no runs, the machine writes \(0\) and halts after its two setup transitions.
Suppose every trace of \(N\) on \(x\) has halted after \(T\) steps, and let \(K = 12s + 1\). If \(N\) accepts \(x\) with probability at least \(2/3\) (clock \(T\)), then \(\mathrm{rep}(N, K, T)\) accepts \(x\) with probability at least \(1 - 2^{-s}\) (clock \(2 + K(2T + 2)\)). If \(N\) accepts \(x\) with probability at most \(1/3\), then \(\mathrm{rep}(N, K, T)\) accepts \(x\) with probability at most \(2^{-s}\).
Combine the exact identity with majority amplification.
3.8 Zero-error randomized computation
\(\mathsf{ZPP}_{\mathrm{LV}}\) is the class of languages \(L\) with a probabilistic machine \(N\) and a polynomial \(T\) such that every trace on every input \(x\) halts within \(T(|x|)\) steps with output either the correct verdict \([x \in L]\) or a designated “don’t know” answer, and the probability of “don’t know” is at most \(1/2\). (The textbook expected-polynomial-time formulation needs an expected-time machine semantics, which the library does not have.)
\(\mathsf{ZPP}_{\mathrm{LV}} = \mathsf{ZPP}\), where the library defines \(\mathsf{ZPP} = \mathsf{RP} \cap \mathsf{coRP}\). This is the fixed-clock half of Theorem 160.
A Las Vegas machine gives an \(\mathsf{RP}\) machine by answering \(0\) on “don’t know”, and symmetrically a \(\mathsf{coRP}\) machine. Conversely, run the \(\mathsf{RP}\) and \(\mathsf{coRP}\) machines and answer only when one of them certifies the verdict; “don’t know” then has probability at most \(1/2\), with no amplification needed.