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.
Probabilistic polynomial time machine interface
Definition
A probabilistic Turing machine (PTM) is a fixed multitape machine with two total ordinary transition tables. At each nonhalting transition a fresh independent fair bit selects the table. It is polynomial time if one fixed integer polynomial p bounds the number of transitions on every random branch on every input x by . This is a worst-case branch bound, using Polynomial time verifier and reduction interface, not an expected-time bound.
For an input of length n, probabilities may be defined on the finite space , giving every word mass . A deterministic simulator uses bit j for transition j and ignores unused suffix bits after halting. Acceptance probability is the sum of masses of words giving acceptance. Independence has the finite-variable meaning of Pairwise and mutual independence of finite-valued random variables. The finite probability space is not itself storage charged to the machine.
Facts & Assumptions
Given: A PTM with the displayed all-branch bound p.
Mutual independence means that every prescribed finite set of coordinate values has joint probability equal to the product of its marginals (Pairwise and mutual independence of finite-valued random variables).
Verification
A fixed prefix of j bits occurs in words, hence has mass . More generally, prescribing any j distinct bit positions leaves free coordinates and has the same count. Each marginal is one half, and the joint probabilities factor, exactly as in F1. The empty prescription has mass one.
For a fixed supplied word, the simulator and the PTM take the same first table, and agreement through transition j makes them use the same table and configuration at the next transition. Thus they agree up to the halt by induction. A branch halting after j steps corresponds to precisely the words with that consumed prefix, of total mass ; prefixes for distinct terminal branches are disjoint. Summing their masses proves agreement with fresh fair-bit semantics, even when the stopping time depends on previous bits. Unused suffixes have been counted, not assumed independent of a stopping rule. For p(n)=0 the space is the singleton containing the empty word; in a model with nonhalting start such a bound is impossible on that input, which is consistent with the definition.
Depends on
Used by
- Rp corp zpp bpp and pp classes Definition
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
- Arora–Barak §7.1, Definitions 7.1 and 7.4 (standard reference, not scraped)