ExampleConstruction: Literature-sourcedVerification: 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.

Budgeting a time-diagonal language

Example

Fix one candidate pair $(M, c)$ , with positive integer multiplier $c$ , in the clocked diagonal construction of The time-diagonal language respects its budget. For sufficiently long padded codes of this fixed pair, decoding, constructing the clock $c f (n)$ , and simulating it fit within any fixed positive fraction of $g (n)$ . The required padding threshold may depend on $M$ and $c$ .

Facts & Assumptions

Given: time-constructible $f, g$ with $n \leq f (n)$ eventually and $f \log f = o (g)$ , a fixed pair $(M, c)$ , and its padded codes of length $n$ .

Verification

technique · direct

1.1

For this fixed pair, decoding costs $O_{M} (n)$ , clock construction costs $O_{c} (n + f (n))$ , and simulation costs $O_{M} (n + c f (n) \log (c f (n) + 2))$ . Since $c$ is fixed and $f (n) \geq n$ eventually, their sum is $O_{M, c} (f (n) \log (f (n) + 2)) = o (g (n))$ .

givenalgebra

2.1

Therefore, for every fixed reserve $ε > 0$ , there is $N_{M, c, ε}$ such that all these padded codes of length $n \geq N_{M, c, ε}$ fit within $ε g (n)$ simulation time. Complementing the terminal answer adds constant time. Shorter codes can take the construction's timeout/default branch; no common padding threshold or simulation constant over all pairs is claimed.

step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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 and Barak, Computational Complexity, §3.1 (standard reference, not scraped)