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 vertices and words of length on their labels
Statement
For every natural , Prüfer encoding is a bijection from the set of trees with vertex set to the set of words of length on . 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 .
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).
Decoding is well defined and produces a labelled tree (The Prüfer decoding procedure is well defined and produces a labelled tree).
Two maps are inverse bijections when both composites are identity maps (Injection, surjection, bijection).
Induction is valid on the word length (The principle of mathematical induction).
Decoding chooses the least unused label absent from the remaining word, attaches it to the first remaining symbol, and then deletes that symbol.
Proof
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.
Assume that encoding and decoding are inverse on every finite natural-label set of size .
Let and let be the least label absent from . Decoding first attaches to and never uses again.
Conversely, let be a labelled tree, let its first encoding operation delete the least leaf , and let it record the neighbour .
In the decoded tree, is a leaf. Every label smaller than occurs in , 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 and records .
The label 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 is the least label absent from the code, and decoding first restores the edge .
After removing and the first word entry, both procedures operate on the same ordered label set of size and the suffix word. The induction hypothesis shows that the remaining operations are inverse. Thus encoding the decoded tree returns .
After deleting and the first code entry, the induction hypothesis restores the remaining tree on its ordered label set of size . Therefore decoding the code of returns .
Both composites are identities, so encoding and decoding are inverse bijections on the ordered label set of size . Applying this to the natural order on proves the theorem.
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
- ISI Bangalore discrete mathematics notes, Trees and Cayley’s theorem (standard reference, not scraped)