Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Prüfer encoding and decoding are inverse bijections between labelled trees on n2n\ge2 vertices and words of length n2n-2 on their labels

Statement

For every natural n2n\ge2, Prüfer encoding is a bijection from the set of trees with vertex set nn to the set of words of length n2n-2 on nn. Its inverse is the decoding procedure of The Prüfer decoding procedure is well defined and produces a labelled tree.

Facts & Assumptions

Given: A natural number n2n\ge2.

[F1]

Encoding repeatedly removes the least labelled leaf and records its neighbour (The Prüfer code of a tree on a finite set of natural labels).

[L1]

Decoding is well defined and produces a labelled tree (The Prüfer decoding procedure is well defined and produces a labelled tree).

[F2]

Two maps are inverse bijections when both composites are identity maps (Injection, surjection, bijection).

[L2]

Induction is valid on the word length (The principle of mathematical induction).

[F3]

Decoding chooses the least unused label absent from the remaining word, attaches it to the first remaining symbol, and then deletes that symbol.

Proof

technique · induction on the size of the label set. We prove the stronger statement for every finite set of natural labels with its inherited order
1.1

On a two-element natural-label set, the only word is empty and the only tree is the edge joining the labels, so encoding and decoding agree.

baseF1L1
1.2

Assume that encoding and decoding are inverse on every finite natural-label set of size n1n-1.

ih
1.3

Let w=a0an3w=a_0\cdots a_{n-3} and let vv be the least label absent from ww. Decoding first attaches vv to a0a_0 and never uses vv again.

chooseF3L1
1.4

Conversely, let TT be a labelled tree, let its first encoding operation delete the least leaf uu, and let it record the neighbour bb.

chooseF1
2.1

In the decoded tree, vv is a leaf. Every label smaller than vv occurs in ww, so while it is unused it receives an edge as a recorded neighbour and later receives its deletion edge or the final edge. Hence no smaller label is initially a leaf, and encoding first deletes vv and records a0a_0.

step 1.3F1
2.2

The label uu is absent from the full code. Every smaller label is not initially a leaf, so before it can be deleted, deletion of an incident leaf records it at least once. Thus uu is the least label absent from the code, and decoding first restores the edge ubub.

step 1.4F3
3.1

After removing vv and the first word entry, both procedures operate on the same ordered label set of size n1n-1 and the suffix word. The induction hypothesis shows that the remaining operations are inverse. Thus encoding the decoded tree returns ww.

step 1.2step 2.1L2
3.2

After deleting uu and the first code entry, the induction hypothesis restores the remaining tree on its ordered label set of size n1n-1. Therefore decoding the code of TT returns TT.

step 1.2step 2.2L2
4.1

Both composites are identities, so encoding and decoding are inverse bijections on the ordered label set of size nn. Applying this to the natural order on nn proves the theorem.

step 3.1step 3.2F2discharge-induction

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 48 results over 27 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources