ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-12

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.

A computation-history domino system whose matches spell a halting run

Example

Let $M$ be the one-tape machine that, on the one-symbol input 1, has the transition $δ (q_{0}, 1) = (q_{a c c}, 1, L) .$ The head starts at the left boundary, so the left move is clamped there. Its accepting history has two configurations: $C_{0} = q_{0} 1, C_{1} = q_{a c c} 1.$

With the fresh left marker $▹$ , the construction of Accepting computation histories can be encoded by modified-PCP domino matches therefore contains the exact dominoes

$(#, # ▹ q_{0} 1 #), (▹ q_{0} 1, ▹ q_{a c c} 1), (#, #),$

together with the copier $(1, 1)$ , the accepting-cleanup dominoes $(▹ q_{a c c}, q_{a c c})$ and $(q_{a c c} 1, q_{a c c})$ , and the terminal domino $(q_{a c c} # #, #)$ .

Facts & Assumptions

Given: The toy machine $M$ above and its two-step accepting history.

[L1]

The computation-history construction gives the displayed start, clamped-left transition, and separator dominoes, and the resulting instance has a match exactly when the machine has an accepting history, by Accepting computation histories can be encoded by modified-PCP domino matches.

Verification

technique · direct

1.1

Choose the three displayed dominoes in order. Their top concatenation is $# ▹ q_{0} 1 #,$ while their bottom concatenation is $# ▹ q_{0} 1 # ▹ q_{a c c} 1 # .$ Thus the top has matched the initial block and the bottom is exactly one block ahead with the accepting configuration. No right-boundary extension is needed because the only move is the clamped left move.

L1givenconstruct

2.1

After the three dominoes in step 1.1, append $(▹ q_{a c c}, q_{a c c}), (1, 1), (#, #), (q_{a c c} 1, q_{a c c}), (#, #), (q_{a c c} # #, #) .$ Every pair belongs to the construction in [L1], and the two complete rows are both $# ▹ q_{0} 1 # ▹ q_{a c c} 1 # q_{a c c} 1 # q_{a c c} # # .$ Thus this instance has a match. Conversely, [L1] decodes every match back to an accepting history; here determinism leaves only $C_{0}, C_{1}$ . The theorem The modified Post correspondence problem is undecidable says that no algorithm can decide all such instances, even though this particular accepting instance is visible directly.

L1step 1.1construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

Chris Pollett, CS 154: PCP and Rice's Theorem (standard reference, not scraped)