DefinitionDefinition: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)

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.

Computable many one reducibility interface

Definition

For $A, B \subseteq N$ , write $A \leq_{m} B$ if a total computable $f : N \to N$ satisfies $\forall n \in N (n \in A ⟺ f (n) \in B) .$ Computability uses Kleene normal form for the fixed machine coding and the encoded partial-function meaning of Partial functions computed by a machine under fixed encodings. Direction is from the membership problem A to the target B.

For an oracle $X \subseteq N$ , $A \leq_{m}^{X} B$ has the same definition with f total X-computable. An oracle program is a finite ordinary tape program augmented by a query tape and a query instruction: when its tape contains a canonical numeral, receive in one query transition the bit indicating membership of that number in X; malformed queries receive zero. Writing the query costs ordinary transitions. This convention does not assert that X is computable.

For languages over fixed finite alphabets, $L \leq_{m} K$ instead means a total string-valued computable map f with $x \in L$ iff $f (x) \in K$ on every source word. In the numeric-to-string bridge below, only canonical input numerals have a membership requirement, and their outputs must be canonical. This is not a claim about reductions between unrestricted numeral-image languages.

Facts & Assumptions

Given: The definitions above, canonical numeral parsing and finite tape routines. The bridge is restricted to canonical numeral inputs and outputs.

[F1]

The normal-form theorem supplies machine computability and strict composition of computable routines (Kleene normal form for the fixed machine coding).

Verification

1.1

Identity is total computable and preserves membership, so $A \leq_{m} A$ . If f reduces A to B and g reduces B to C, compute f then g; both halt on every natural, and $n \in A$ iff $f (n) \in B$ iff $g (f (n)) \in C$ . The same sequential program works with oracle X for both routines, routing each query to X. String-valued identity and composition obey the identical membership calculation.

F1given

2.1

Given a numeric reduction f, parse a source word. On a canonical numeral for n, add the numeric machine's tuple wrapper, run f, decode its numeric result and output $bin (f (n))$ . On malformed input output the one-letter zero. This is total and meets precisely the canonical-input specification. Conversely a total string map having canonical outputs on all canonical inputs gives a total numeric map by forming $bin (n)$ , running the map, and decoding its canonical output. The iff of membership is preserved in each direction. These finite encoders/decoders work unchanged relative to X. Malformed input is outside this bridge's specification; choosing zero there would not in general reduce the full numeral-image language if $0 \in B$ .

F1step 1.1given∎

Depends on

Used by

Oracle turing reducibility interface Definition

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

Patey chapter 5, Definitions 4.1 and 5.2, pp.87–89 (design locator, independently unread) (standard reference, not scraped)