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.
Unbounded error time space counting model
Definition
Use fixed finite-control fair-bit probabilistic machines with read-only binary input followed by blanks and a fixed finite number of work tapes and heads, with a finite explicit transition-table code. Each nonhalting transition consumes one independent fair bit as in Probabilistic polynomial time machine interface. Fix one access profile for each complexity class.
In the sequential profile, heads move locally by at most one cell per transition. In the erased-index head-access profile, use the head-access mechanism of the final 2012 Van Melkebeek–Watson model: a zero-initialized binary classical work tape, a fixed finite number of input/work heads, and classical finite control. Each head may move left, right, stay, or jump in one transition to an address computed on a designated one-way sequential-access write-only index tape. Index tapes are initially empty, writing each bit is charged to the ordinary transition count, and an index tape is erased after each use. The original input tape is read-only and contains the input followed by blanks. If coincident work heads make an operation undefined, omit that work-tape operation in the transition. All heads start at the left boundary; left motion there clamps at zero.
The published VMW derived basis restriction, denoted the basis profile, also permits the classical basis action of the source's native coherent input query. On a contiguous block of a specified binary work tape, the first bits give the binary input index in most-significant-first order and the last cell holds ; the query replaces only by , using zero on invalid input indices. Both endpoints are freshly emitted on erased index tapes. The native query costs one transition, as in the published quantum model. The input indices are , with ; the empty address word denotes zero, and reversed endpoints cause omission of the query. Allow a fixed finite number of binary work tapes, local operations of fixed finite arity, and native queries on any specified tape: this is the fixed finite product of these classical basis operations, permitting separate path-simulation rows. This is an explicit locally defined comparison model derived from the quantum operations. The source does not separately state a formal classical block-query machine definition, and no equivalence with the index-only profile is assumed. The clocked-normalization lemma proves the required time-only simulation into that profile for clocks at least the input length; no general sublinear-time equivalence is asserted.
For historical comparison, the preprint-delimited VMW profile retains the 2007 preprint convention: a jump reads the address written between two classical work-tape heads, without the final paper's write-only erased index tapes. This is a separately named profile. No equivalence or preservation of time/space bounds between the preprint-delimited and published profiles is asserted. Results proved below for the published profile do not establish their extension to the preprint-delimited profile.
Time is the maximum number of transitions on every branch. Sequential space counts distinct visited work cells. Erased-index and basis space use the maximum address of every work cell accessed on any branch, including the highest endpoint of every native basis-query block; read-only input and index tapes are not counted in this maximum-address measure. The preprint-delimited space convention is likewise its maximum visited work-head address. For a fixed profile, uses strict acceptance probability greater than on members and at most on nonmembers; adds the stated space bound. Subscripts , , , and distinguish the four profiles. An exact classical oracle is deterministic; writing its queries and returning from them are charged, and total query-string length is at most the outer running time.
For either , define and . Oracle queries are exact and all fair-bit branches belong to the outer machine. An omitted profile in an item must be fixed explicitly by that item's hypotheses; profiles are never silently identified.
A formula has a fixed finite set of Boolean variables and is accepted when at least half of assignments satisfy it. A formula has two disjoint ordered variable blocks and is accepted when at least half of outer assignments leave a residual formula true on at least half of inner assignments. Use a common explicit plain-formula encoding for MajSAT. MajMajSAT accepts this same plain encoding with one implicit fresh unused outer variable and all formula variables in the inner block; it also accepts a separately tagged encoding with the two variable blocks explicitly listed. Thus every plain MajSAT instance embeds identically, bit for bit, into MajMajSAT with unchanged truth value. The unused outer variable is part of the decoded fixed finite variable set. Concretely, use distinct fixed tags for plain and partitioned inputs, a unary declaration of the number of variables, fixed-width variable indices, and prefix-encoded binary AND/OR and unary NOT gates (with constant tokens). The partitioned form also gives the outer-block split; variables are renamed into block order. Plain-format validity is checked by one pending-subexpression counter, variable-range checks and a scan of the declared fields, using time and workspace. These conventions do not alter either at-least-half threshold. Malformed encodings are rejected by both problems.
Source-model boundary
The published-profile convention follows Van Melkebeek and Watson, Time-Space Efficient Simulations of Quantum Computations, Theory of Computing 8 (2012), §2.3.1–2.3.2, printed pages 10–11, https://doi.org/10.4086/toc.2012.v008a001. The delimited-head mechanism belongs to the 2007 arXiv preprint. The final-source correction retains that historical mechanism explicitly but grants no theorem about it.
Operand-space clarification
The source informally describes space as maximum work-head address and its simulation proof fixes an -qubit work register. Here operand access is explicit: every local operand and every endpoint of a native query counts as a work-access head for the space measure. This local clarification prevents uncharged query workspace. The source does not explicitly spell out this endpoint rule; it is not quoted as a verbatim source condition. No lower-bound or resource-inclusion claim is made for a literal head-only variant that permits free uncharged query blocks.
Depends on
Used by
- BQTISP Model Definition
- Bounded-overhead tie normalization for fair-bit machines Lemma
- Bounded-space simulation of a generated input Lemma
- Counting time space to linear hierarchy Lemma
- Logspace predicates in a fixed linear counting hierarchy level Lemma
- Logspace uniform near-linear Cook formula encoding Lemma
- Tight majority formula completeness Lemma
- Time normalization of classical basis queries Lemma
- Uniform clocked simulation of encoded probabilistic machines Lemma
- BQTISP to Derived-Basis PrTISP Simulation Theorem
- Counting Hierarchy Time Space Lower Bound Theorem
- Probabilistic polynomial time hierarchy Theorem
- Unbounded error counting time space alternative Theorem
Dependency tree · two levels
7 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, Theory of Computing 8 (2012), Sections 2.3 and 5 (standard reference, not scraped)
- Eric Allender et al., Time-Space Tradeoffs in the Counting Hierarchy (standard reference, not scraped)
- Van Melkebeek and Watson, A Quantum Time-Space Lower Bound for the Counting Hierarchy, Sections 2–3 (standard reference, not scraped)