LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-09-06

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.

Padding transfers time bounds

Statement

Let $p : N \to N$ satisfy $p (n) > n$ for every $n$ . Suppose the canonical padding in Language padding is constructible on $x$ in $O (p (∣ x ∣)^{c})$ time, and validity of any string $y$ of length $N$ can be decided, with its unpadded word recovered when valid, in $O ((N + 1)^{c})$ time, for a fixed integer $c \geq 1$ .

If $A$ has a deterministic decider taking $O (t (n))$ time, then ${pad}_{p} (A)$ has a decider taking $O ((N + 1)^{c} + t (n))$ on valid inputs of decoded length $n$ and total length $N = p (n)$ , and $O ((N + 1)^{c})$ on malformed inputs. Its worst-case bound at length $N$ is $O ((N + 1)^{c} + τ_{p} (N))$ , where $τ_{p} (N) = \max ({t (n) : p (n) = N} \cup {0}) .$ Conversely, if ${pad}_{p} (A)$ has a deterministic decider taking $O (u (N))$ time, then $A$ has a decider taking $O (p (n)^{c} + u (p (n)))$ time.

Facts & Assumptions

Given: $p, c$ and the construction/validation procedures above; for the forward implication an $O (t (n))$ decider for $A$ , and for the converse an $O (u (N))$ decider for ${pad}_{p} (A)$ .

Proof

technique · direct

1.1givenconstruct

For the forward implication, validate $y$ and reject it if malformed. Otherwise recover $x$ and run the supplied $A$ decider. By the padding definition its answer is correct, and its cost is $O ((N + 1)^{c} + t (∣ x ∣))$ . Since $p (n) > n$ , the set of lengths $n$ with $p (n) = N$ is finite; maximizing gives the displayed worst-case bound, including lengths with no valid pad.

2.1givenconstruct∎

For the converse, on $x$ of length $n$ construct $x # 1^{p (n) - n - 1}$ and run the independently supplied padded-language decider. The exponent is nonnegative, including at $n = 0$ , and this valid pad belongs to the padded language exactly when $x \in A$ . Construction costs $O (p (n)^{c})$ and the decider costs $O (u (p (n)))$ , giving the claimed sum.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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

Sebastiaan Terwijn, Complexity Theory, Exercise 3.5.2(a) (standard reference, not scraped)