How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Uniform clocked simulation of encoded probabilistic machines
Statement
Fix the explicit complete transition-table coding specified below. There are two distinct fixed finite-alphabet probabilistic interpreters, one for the sequential access profile and one for the erased-index head-access-only random-access profile. Each interpreter simulates valid descriptions with input and an external binary clock , reproducing exactly the source acceptance or rejection reached in at most source transitions and rejecting nonhalting expiry. The simulated fair-bit distribution is exact. Writing and , there are absolute constants such that each simulation takes time For the index-only profile, jump addresses are written on one-way sequential write-only index tapes erased after use; the older nonerasing delimited-head profile is a distinct profile and is not covered by this index-only assertion. The fixed interpreter has a fixed finite physical head count even when the described source head count varies. Malformed descriptions halt rejecting. This is a time simulation; no preservation of the source's simultaneous space bound is asserted.
In particular, for each fixed polynomially bounded time-constructible and fixed , descriptions of length at most are simulated in either one fixed declared profile in time, including the clock constructor. Arbitrary superpolynomial clocks retain the general displayed bound rather than this specialization.
Facts & Assumptions
Given: A code , binary input of length , external binary clock , and one of the two declared profiles. Put . Work without any choice principle.
Unbounded error time space counting model supplies the sequential fair-bit profile and the erased-index head-access-only profile. The latter has ordinary charged one-way write-only index emission and erases an index after each use. Each source transition emits at most one bit on each source index tape. It is distinct from the older preprint's nonerasing delimited-head profile. Both interpreters consume one independent fair bit per simulated source transition.
Effective binary encodings and total decoders defines effectiveness without a complexity guarantee. The explicit table coding constructed below, rather than an arbitrary effective encoding, supplies the required parsing bound.
Time-constructible and space-constructible functions supplies the fixed clock constructor. For the polynomial specialization, both and a fixed polynomial upper bound for are assumed.
Proof
Specify the syntax rather than appealing to an arbitrary effective code. Use canonical binary numeric fields, each encoded as , and encode a tuple of such fields by followed by their encodings. Supply two complete transition tables, one for each fair-bit value. The virtual input tape is read-only, each work tape is initially blank, and each head starts at cell zero with clamped left motion. The finite input alphabet is the two binary input symbols, distinguished from blank. A header lists the tape count , alphabet size , state count , start and two distinct halting states; the two tables list every nonhalting state/scanned-symbol tuple in lexicographic order, each with its next state, written symbols, and local moves or stationary requests. For the read-only tape require its written symbol to equal the scanned symbol. All integers use canonical binary numerals, all blocks carry unary length headers, and the number of blocks is unary-prefixed. Include explicit table delimiters and a profile tag. This is prefix-free, includes each finite machine of the chosen numeric form, and has a total decoder. If the start state is nonhalting, a complete table contains at least one row with symbol/move fields and contains all nonhalting states and scanned symbols, giving , and . An initially halting machine will instead be handled without per-tape initialization by an early return after validation. Each stored integer has at most bits even without these sharper bounds.
For this erased-index interpreter put , and , so and . Use the explicit unary-length tuple syntax from the sequential candidate, now adding finite head labels, the source index-tape labels, a profile tag, index-output actions and native jump actions to each transition row. A row specifies all source actions, and the complete table explicitly includes every state/scanned-symbol/bit case. For nonhalting start states, at least one such row exists, so the number of source heads and index tapes, every alphabet width, and each instruction-record width are bounded by a fixed polynomial in . Initially halting machines use that early return. The source's one binary work tape is included as a special case; any allowed finite additional tapes receive tape labels. Parse and validate by capped expected-count arithmetic without expanding an asserted table; this takes time. State and scanned-symbol lookup by repeated scans of the saved table costs per source transition. The fixed physical interpreter never acquires a new head or an alphabet depending on .
Parse and check the actual blocks without expanding a claimed table. Count the actual rows first; compute expected products and powers by binary arithmetic capped one above that actual count, rejecting excess, invalid ranges, missing rows or extra data. If there are no nonhalting states, the expected row count is zero without computing a power or iterating over tape/head labels. Check each actual row's arity against the binary header by counting its actual fields, never by a loop of header-specified length. This bounds all valid and invalid code processing by a polynomial in : the operands, counters and scans have length , there are actual blocks, and every product/exponent loop is capped or uses at most exponent bits. Ordinary repeated scans and school arithmetic suffice, for example in time and space. After validation, if the start state is halting, report that outcome immediately, even for , without allocating or initializing per-tape or per-head structures. Otherwise the parameter bounds of steps 1.1 and 1.2 apply to all following phases. Preserve a decoded table of length , runtime parameters and fixed-width symbol/state codes of width at most . Copy to a sequential archive and read/copy the clock in time. All subsequent routines use fixed physical tape counts and fixed alphabets; variable-size data remain on tapes.
For each source index tape reserve a separate contiguous region of binary cells, with its current length stored in metadata. Reserve these regions by arithmetic base offsets before the dictionary heap; reservation moves no head through the regions and requires no initialization sweep. A source index emits at most one bit per source transition, so its live word always fits. Appending a source bit writes at its region's base plus current length and increments that length. Use/reset sets the length to zero; future emission overwrites old bits, and reading only the current prefix ignores the discarded suffix. Interleaved emission onto different source indexes therefore never interleaves their physical words. Since at most bits are emitted per source transition, the sum of lengths of all words consumed at jumps, plus lengths still live at expiry, satisfies , up to a harmless fixed-format constant. A jump using one word for several source heads in the same transition multiplies this accounting by at most , still a polynomial in . Reading, copying or canonicalizing each consumed word once, or a fixed number of times per affected head, therefore has total length . The reserved regions' total extent is , consistent with later maximum-address bounds. This charged fresh-writing invariant is exactly what fails for the old nonerasing delimited-head model.
Split each numerical source head address uniquely as , where . Call its block prefix and its short offset. Store the short offset in bits. Maintain a global prefix dictionary assigning one compact integer block ID to each registered numerical prefix. A dictionary key for is the prefix-free word , where is the canonical binary numeral of , including at zero. Use a literal binary trie: each node has two child pointers, an optional terminal block ID and its fixed metadata. Reading/inserting a key follows or creates one node per bit. Numerical equality of prefixes is equality of their canonical words, hence exactly equality of terminal nodes. No balancing, probabilistic hashing, numerical unit-cost large integers or unspecified dictionary theorem is required. Include a tape label in this key when more than one virtual work tape is allowed.
For each virtual tape, store its scanned cell as a centre and the cells on either side as two ordered stacks, nearest cell first. At level , put ; each side has capacity , occupancy or , and complementary occupancies summing to . Initially each side has occupancy at every level; the right stack holds the input suffix on the input tape and blanks elsewhere, and all left stacks are blank. Each record has an immutable origin bit, one exactly for source cell zero; it moves with the symbol record. Genuine records are packed at the near end of each zone, and concatenating zones while ignoring holes gives the stack. Each physical slot has delimited virtual fields, each of width at most , containing a symbol and an immutable origin bit, or a hole. Store the centre fields and the three-valued occupancy flags explicitly. A slot therefore has width ; this uses no alphabet depending on and no additional physical tape for each virtual tape. A stationary move changes only the centre symbol. At the left origin a requested left move also changes only that symbol. For the input tape suppress writes. These modifications preserve the same stack and origin invariants.
On a source head's jump, read the consumed address word, discard leading zeros and split off its final bits as , padding on the left with zeros if the word has fewer than bits. The remaining canonical prefix is , or zero. Form canonical when , and by ordinary binary scans; forming all three costs for address-word length . Register them in the prefix trie. Record their three compact IDs as a private cache for this head, and record that the current block is the middle one. Use a special clamped boundary marker instead of a negative block when . Initialize each source head at address zero with this same cache for zero and one. If several source heads jump to the same address, their numerical prefixes receive the same global IDs. The total number of prefix-trie nodes is at most the total length of all registered keys, hence at most : for each jump, all three prefix keys have length , and step 2.2 charges their summed lengths. Duplicated registrations only decrease the node count. Tape-label overhead adds at most bits per jump.
Implement a move to the right by first writing the old centre and choosing the least with a nonempty right zone. All lower right zones are empty and their left partners full. Remove the first records of right zone : the first becomes the new centre, and the remaining fill the lower right zones in order, per zone. Right occupancy at level decreases by . Prepend to the concatenation of the lower left zones. The resulting records split into a first list of length , distributed in order half-full among the lower left zones, and a remaining list of length , prepended to left zone . Its previous occupancy was zero or , so no capacity is exceeded. Both stacks keep their order, complementary occupancies at level are preserved, and every lower zone becomes half-full. For these instructions simply exchange a stack record with the centre and push the old centre on the other stack. A left move interchanges left and right; at the origin it only writes the centre. Untouched higher zones are half-full, so a source zone always exists. Thus every operation preserves the representation and performs exactly the prescribed source move.
Between two jumps of this head, its address changes by at most in total absolute distance from its most recent jump address, since every local move changes it by at most one and there are at most source transitions altogether. As , every intervening address belongs to one of the three blocks cached at that jump. A local move updates the -bit offset; overflow/underflow switches to the appropriate adjacent cached ID and wraps the offset. Store the current cache position as one of three finite values. Even if the head crosses the same block boundary many times, the existing IDs are reused, with no re-reading or arithmetic on long prefixes. From the lower cached block it cannot cross to an uncached lower block, and from the upper cached block it cannot cross to an uncached upper block: either would require more than local moves since the jump. Clamp a left move at numerical zero. Thus the pair (current block ID, short offset) is always an exact address representation, with bits after accounting for the polynomial number of trie nodes.
Make the scan algorithms uniform as follows. To process virtual field , keep a unary field index of length at most ; at each slot count through the delimited fields, copy or replace just field , and copy the other fields unchanged. A full slot, its index operations, and returning a scratch head across the bounded parameter records cost at most . The same bound covers building one fresh slot by copying the saved width and tape-count templates. Midpoint/end markers specify half-zones, so the scans need no growing arithmetic per record. Copying the selected genuine field records to scratch, distributing the prescribed lists, restoring holes and flags, and returning the physical heads use a fixed number of prefix scans for step 4.1; at level they traverse slots. Endpoint and optional level-label overhead is also , since the sum of the binary level-label lengths through is . Thus the work for a level- event on one virtual tape is at most , uniformly in . This deliberately generous bound includes scans to find the least nonempty source zone, scratch copying, occupancy changes and allocating new levels by doubling the preceding unary capacity marker. Each operation is a scan, a finite-width copy, or an index operation of length at most ; no unit-cost random memory operation is being assumed.
The event count is independent of field width. Fix a virtual tape and . Its right occupancy below level starts at . Each event at level at least resets it to ; a lower-level positive or negative move changes it by minus or plus one, and a stationary or clamped move leaves it fixed. An event at level at least requires the appropriate lower stack empty, hence occupancy zero or immediately beforehand. It therefore requires at least preceding lower-level moves and then its triggering transition. Among simulated transitions there are at most such events, including the first. Level zero has at most events, and no level with is reached. The redistribution in step 4.1 resets all lower zones even when its level is strictly larger than ; successive operations on different virtual tapes do not change each other's fields.
Maintain a second literal binary trie for virtual work cells, keyed by the compact block ID and the -bit offset, with explicit length delimiters (and virtual tape label if needed). The key length is . Every terminal stores the virtual symbol, initially zero/blank on first lookup. Each source transition touches at most virtual cells, so there are at most terminal keys and nodes in this trie. All keys with the same virtual cell get the same terminal, regardless of which source head or which jump registered that prefix. Source work-tape collisions can therefore be detected by comparing these compact address pairs for all relevant heads, in work per transition. Omit precisely the operations declared undefined by the source's collision convention. Read all source scanned symbols and save all source instructions before any virtual write or move.
Initially retain the input archive at position one and initialize only the centres. On first allocating level , fill the first virtual tape's untouched right half from the next archive symbols, then blanks after exhaustion; initialize the other virtual fields with blank and unoccupied halves with holes. Levels are allocated in increasing order, and lower operations do not alter that untouched suffix, so every archive symbol is consumed at most once. A new level uses only the work charged to the event reaching it. Initially right zone represents source positions ; hence the archive is exactly at the next untouched interval. Slot creation and symbol coding are charged by step 5.1. Thus no full distribution pass is hidden in initialization.
Before each virtual transition, test the saved state, then test expiry. If still nonhalting with positive countdown, consume one fresh fair bit to choose the corresponding decoded table. Deterministically scan its rows and compare the source state/scanned-symbol tuple with the saved state and centres, copying the unique instructions into scratch. At most rows and saved fields are involved; repeated full scans and resets take per transition. Save all instructions before applying any virtual write/move, process the buffer operations in order, then update the state and decrement the binary countdown. Test the new halting state before the next expiry test, so a halt on transition is reported. A whole countdown scan costs per virtual transition. At the nonhalting initial configuration expires immediately.
Treat read-only input separately. Since , an input-head address is in range only if its block prefix is zero and its short offset is an input position. The global trie has the distinguished ID for zero, so this is a comparison of compact IDs followed by comparison of -bit integers. On an in-range address issue a native input query with the original short address, or its fixed encoding-offset translation if the physical interpreter input is a paired encoding of . This translation has bits. On an out-of-range address return the source's prescribed blank. The same compact head representation implements local input moves and jumps. The original input is never expanded into the work-cell trie.
Store the two tries, the reserved source index-word regions, finite-program records, per-head caches, short counters and scratch on allocated regions of the interpreter's single binary classical work tape. Encode record delimiters and symbols by constant-length binary blocks. Long key/input-word arrays have total length ; trie nodes and other records have length . The cell trie has nodes by step 5.3. Consequently every physical location used is below , and every pointer has bits. No source's enormous numerical address is used as a physical memory location. Reserve the polynomially sized source-program/scratch region and the source-index regions by arithmetic offsets, then use a global high-water counter to append-allocate the dictionary heap and saved long keys. This reserves address intervals without writing their unused cells.
Buffer correctness from step 4.1 and the saved-instructions ordering imply by induction that after each virtual transition the interpreter stores the exact virtual configuration prescribed by the consumed bits. Although the physical probabilistic machine receives a bit at every physical transition, ignore all of them except at the designated virtual-choice operation. Conditional on every past consumed bit and the corresponding completed deterministic simulation, the next designated bit is still unbiased and independent: its location depends only on previous bits, and disjoint future coordinates of a finite independent-bit string have the prescribed fair conditional law. Equivalently, for each fixed virtual choice prefix of length , induction on its successive designated choice operations gives probability ; ignored physical bits have total conditional probability one. Terminal virtual prefixes are disjoint. Summing their masses proves exact agreement of acceptance/rejection/timeout probabilities, including branch-dependent halt times.
Summing step 5.1 using step 5.2, first for each tape and then over , bounds total buffer and lazy-allocation work by when . Add polynomial code processing, the input archive scan, transition lookup, and the binary-clock work. The physical heads move locally by at most one cell per transition, as required by the sequential profile. Enlarging the absolute exponent to and the constant covers all contributions, the binary-clock input length, and . This proves the general displayed bound.
Choose one pointer width at initialization, for an absolute constant exceeding all fixed exponents in step 6.4. Node-count and record-length bounds there imply that the allocated region is smaller than ; indeed its logarithm is . Thus all pointers, lengths and allocation counters can be padded to bits, and every trie node has fixed-width updatable pointer fields; no shifting of a long suffix or variable-record reallocation is needed. A fixed set of physical work heads accesses a record by emitting its short physical pointer on its own one-way erased index tape, taking transitions, making the native jump, and reading or updating that record by local scans. Pointers, offsets and record metadata have polynomial-in- times logarithmic length, so each trie-node operation and each elementary bit-array read/copy takes physical transitions. Each concrete record operation is a bounded number of short-address accesses, scans, and ordinary binary arithmetic. This constructs a fixed-head interpreter in the same erased-index profile; its address emission is charged, and no head count depending on has been assumed.
If and for fixed , then and . Construct unary by a sequential input scan, run the fixed constructor in [F4], and use its binary output as . Since , initialization, construction and simulation together use time. The interpreter's simulated transitions remain sequential throughout. This proves the stated specialization without asserting a corresponding bound for arbitrary superpolynomial clocks or for VMW jumps.
Sum the work. Prefix registration uses key-bit operations by step 2.2 and step 3.2, plus at most splitting/offset work per jump. Every source transition performs program/head/short-counter operations and at most work-cell-trie lookups, each traversing nodes. Native input queries and the binary countdown take polynomially many short-record operations per source transition. Multiply by step 7.3's cost per operation, add the initial input scan and polynomial code parser, and enlarge one absolute exponent to obtain the proposed time bound. Step 6.4 independently bounds maximum physical work-head address by that time bound. This normalization is for time-only use: it does not preserve the original source's smaller space bound.
At each simulated configuration, test the source halting state before expiry. If nonhalting and the countdown is positive, take one designated fresh fair bit, select the source table, perform the deterministic operations above, and decrement. The dictionaries preserve exact source-cell equality and values, the prefix/offset invariant preserves exact head addresses, and the index arrays preserve exactly the source's newly written addresses and erasure. Induction on source transitions therefore reproduces the full source configuration up to expiry, including simultaneous actions and source collision semantics. A halt on transition is reported; a still-nonhalting configuration at expiry rejects. Ignore physical fair bits at all operations except the designated one-per-source-transition choice. Conditional on each consumed prefix, the next designated bit is an independent fair bit, so each source choice prefix of length has mass . Summing over disjoint terminal choice prefixes proves exact probability preservation.
For and fixed polynomially bounded , both and are polylogarithmic in . The displayed general bound is consequently . Scanning to construct unary costs . Its fixed deterministic time-constructible constructor runs in sequential time. Execute that fixed local-move machine using the already proved external-clock erased-index interpreter with successive budgets , restarting from its initial configuration until it halts and yields the binary clock. This uses no advance knowledge of : the last budget is , the sum of the budgets is , and the repeated input scans cost . Since is polynomially bounded and at least , the whole constructor simulation is , absorbed in the specialization. A deterministic constructor ignores the interpreter's designated fair bits. The sequential interpreter of phases 1–4 gives the specialization for the sequential profile. Neither argument identifies the erased-index profile with the old delimited-head profile.
Remarks
The proof uses distinct interpreters for the two profiles. The erased-index representation stores dense dictionaries proportional to the time used; it supplies no VMW-to-sequential simultaneous time/space bridge. The source-space coordinate therefore cannot be transported through this lemma in a counting time/space argument.
The index-only interpretation uses the final 2012 erased-index convention. It is distinct from both the derived full-basis comparison profile and the older 2007 delimited-head profile; no equivalence is asserted here.
Depends on
Used by
Dependency tree · two levels
8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Van Melkebeek and Watson, Time-Space Efficient Simulations of Quantum Computations, final published model, Sections 2.3.1–2.3.2 (standard reference, not scraped)
- Arora and Barak, Computational Complexity, Appendix 1.A (standard reference, not scraped)