LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01

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.

The Prüfer decoding procedure is well defined and produces a labelled tree

Statement

Let $S \subseteq N$ be finite with $∣ S ∣ = n \geq 2$ , and let $(a_{i})_{i < n - 2}$ be a word on the label set $S$ . The following procedure is well defined and produces a tree on $S$ :

At stage $i$ , choose the least unused label absent from the remaining word $a_{i} \dots a_{n - 3}$ , join it to $a_{i}$ , and mark it used. After all symbols are processed, join the two unused labels.

Facts & Assumptions

Given: A word $(a_{i})_{i < n - 2}$ on a finite set $S \subseteq N$ of cardinality $n \geq 2$ (The cardinality $∣ A ∣$ of a finite set).

[L1]

A word with $r$ positions cannot contain more than $r$ distinct labels. Thus among $r + 2$ available labels at least two are absent; every nonempty set of natural labels has a least element (The pigeonhole principle on $N$ , The well-ordering principle).

[F1]

A tree is a connected acyclic graph (Trees, forests, leaves and isolated vertices).

[L2]

Induction applies to the decoding stages (The principle of mathematical induction).

Proof

technique · induction on the stage number

1.1

Before any word entry is processed, the graph has $n$ singleton components indexed by $S$ , each containing exactly one unused label.

base

1.2

Assume that after $i$ stages the built edges form a forest and every component contains exactly one unused label.

2.1

There are $n - i$ unused labels and $n - 2 - i$ entries in the remaining word. Hence at least two unused labels are absent from that word, so the least such label $v$ exists. Every label used at an earlier stage was absent from the then-remaining word and hence from its current suffix, so $a_{i}$ is unused; because $a_{i}$ occurs in the remaining word, $v \neq a_{i}$ .

step 1.2L1

3.1

The label $a_{i}$ lies in a component different from the component containing $v$ : by the induction hypothesis each component contains exactly one unused label, and $a_{i} \neq v$ . Adding $v a_{i}$ and marking $v$ used joins those components without a cycle and leaves exactly one unused label in the new component. Thus the invariant holds after stage $i + 1$ .

step 1.2step 2.1

4.1

Induction gives the invariant after all $n - 2$ word stages. Exactly two unused labels and two components remain; joining those labels makes the graph connected without creating a cycle.

step 3.1L2

5.1

The output uses all labels in $S$ and is connected and acyclic, hence is a labelled tree on $S$ .

step 4.1F1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

28 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

ISI Bangalore discrete mathematics notes, Trees and Cayley’s theorem (standard reference, not scraped)