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.
Turing-Machine Configuration Boundary Interface
1 · Prerequisites
- Construction of the Natural Numbers
- Countability and Uncountability
- Finite Counting, Factorials and Binomial Coefficients
- Formal Languages, Encodings, and Decision Problems
- Linear Recurrences and Rational Generating Functions
- Relations, Functions, and Quotients
- The ZFC Axioms and the Basic Set Constructions
2 · Summary
This page fixes a raw Turing-machine tuple and its boundary conventions: finite-support tapes on natural-number cells, initial head position zero, and machine-relative accepting and rejecting states. The definition verifies that each input supplies a unique valid initial configuration and that the designated outcome predicates are disjoint. These interfaces concern initial and halting configurations; computation sequences belong to the subsequent treatment.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Initial tapes and machine-relative halting configurations
Definition
A raw Turing-machine tuple is where are finite sets, is the blank symbol, , the three designated states are pairwise distinct, and is a total function. The direction tags are distinct. There are no transition entries at halting states.
A tape for this tuple is a function with finite support Write for the set of these tapes. A configuration is a triple . The tape has cells . The left-boundary convention leaves a left-moving head at zero when it is already at zero; at a positive cell it moves to its predecessor. Right movement increases the cell number by one. No permanent end marker is imposed.
For an input word in the convention of Computation alphabets, words, the empty word, and , define Thus the initial head scans the first input cell for nonempty input, and cell zero for empty input. In both cases it is a valid tape coordinate.
Relative to , a configuration is accepting iff , rejecting iff , and halting iff . It is nonhalting otherwise. These are predicates on configurations, not claims that configurations are reachable. The initial configuration is always nonhalting.
Facts & Assumptions
Given: The raw tuple above, with blank excluded from and three pairwise distinct designated states. Work in ZF without choice.
A function on a domain has exactly one value there and takes values in its specified codomain (A function is a relation with and implying ; , the value , domain and codomain); all functions form the set (The set of all functions ).
A word of length is a function ; the empty word has domain zero (Computation alphabets, words, the empty word, and ).
Naturals contain zero and each natural is the finite initial segment of its predecessors (The natural numbers (von Neumann)); its cardinality is (The cardinality of a finite set).
Every subset of a finite set is finite (A subset of a finite set is finite, with , and equality holds if and only if ).
Cartesian products are sets of the specified ordered pairs (The Cartesian product ); Separation forms the subset of an ambient set satisfying a formula with fixed parameters (The Axiom Schema of Separation: for each formula , ).
Verification
The ambient tape functions form the set . For any such , its support is the subset of satisfying ; Separation forms this set. Separating those functions whose supports are finite forms . Taking the product gives the configuration set . Each separating formula uses the fixed tuple as parameters and does not mention the resulting set as a free variable.
Fix . For each , exactly one of and holds. In the first case exists uniquely and belongs to ; in the second the assigned blank belongs to . Thus the graph of the displayed prescription, separated inside , defines a unique total .
If , blank exclusion gives , so . Conversely rules out , since that clause would give ; hence . Therefore , which is finite with cardinality . In particular any subset of the occupied cells is finite. Thus .
If one configuration were both accepting and rejecting, its state would satisfy , contrary to their distinctness. Conversely every state equal to satisfies the accepting predicate and cannot satisfy the rejecting one, and every state equal to satisfies the rejecting predicate and cannot satisfy the accepting one. Membership in the displayed two-element set is equivalent in both directions to one of these equalities, so the halting configurations are precisely the union of these two disjoint classes. Each class is a subset of the configuration set given by its state equality.
For , there are no indices , so everywhere and the support is empty. For , its value at zero is and all cells are blank, so its support is . In general the last occupied cell is when , and cell is blank. Since and , is a configuration for every input, including both these cases. If only the length-zero case occurs.
The state of is , distinct from both halting states. It therefore satisfies neither halting equality and is nonhalting, for every . The left endpoint zero remains a natural coordinate under the clamped convention. Neither this endpoint rule nor the boundary predicates assert that any transition has occurred. Empty or one-state cannot satisfy the tuple hypotheses; the tape alphabet can be just when the input alphabet is empty. Thus the construction and all boundary assertions require no extra nonempty selection or computational assumption.
Source conventions
Savage, §5.1, Definition 5.1.1, pp. 210–211 supplies a single-ended tape with left-adjusted input, but uses a single accepting halt and abnormal termination at the left edge. Watrous, Lecture 12 §12.1, Definition 12.1 and configuration discussion, pp. 120–124 supplies a transition domain excluding two halting states, but uses a two-sided tape and starts the head on the blank preceding the input; his definition only requires the two halting states to be distinct. Sipser, MIT Lecture 5, slides 8–10 uses a right-infinite tape and two designated outcomes, with syntactic transition entries on all states. The precise tuple, pairwise distinct start state, head-at-zero rule, and clamped boundary above are the conventions fixed here. No equivalence between these variants or theorem about runs is assumed.
5 · Examples, counterexamples and false statements
None yet.