ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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 uniquely decodable binary code that is not prefix-free

Facts & Assumptions

Given: The binary code on the two-symbol alphabet ${1, 2}$ defined by $C (1) = 0$ and $C (2) = 01$ .

[F1]

Finite binary source codes, extension, and expected length: The extension $C^{*}$ concatenates the codewords, and the code is uniquely decodable exactly when this extension is injective on all finite source words.

[F2]

Binary prefix codes and their code trees: A prefix code has no codeword that is a proper prefix of a different codeword.

[F3]

McMillan inequality for finite binary uniquely decodable codes: Every finite binary uniquely decodable code satisfies $\sum_{i} 2^{- ℓ_{i}} \leq 1$ .

Example

The word $0$ is itself assigned to symbol 1 and is also the first bit of the word $01$ assigned to symbol 2. Thus the code fails the prefix condition. The next verification shows that the two codewords still admit a unique parse.

Verification

1.1F2given

The codeword $C (1) = 0$ is a proper prefix of $C (2) = 01$ , so [F2] shows this code is not prefix-free.

1.2F1F2giveninduction

Every codeword begins with $0$ . If an encoded word begins with $01$ , its first codeword must be $01$ , since choosing $0$ would leave an unread suffix beginning with $1$ , and no codeword begins with $1$ . If the unread word begins with $00$ , or consists only of $0$ , its first codeword must be $0$ . Repeating this forced rule on the remaining suffix consumes one or two bits at each step and ends after finitely many steps; the empty word is produced only by the empty source word. Hence every encoded word has a unique source parse, and [F1] gives unique decodability.

2.1F3step 1.2algebra∎

The lengths are $1$ and $2$ , so the Kraft sum is $2^{- 1} + 2^{- 2} = 3 / 4 \leq 1$ , consistent with [F3]; this calculation is only a necessary-bound check, while unique decodability was proved in step 1.2.

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

Stanford EE376A, Information Theory Course Notes, Chapter 4: Lossless Compression (standard reference, not scraped)