A reduced tree diagram is unique
ProvedCannonFloydParry.isReduced_represents_uniqueIf two reduced tree diagrams both represent the same element of , they are equal — the same domain tree and the same range tree.
With the previous statement this gives the canonical bijection between and the set of reduced tree diagrams.
import Definitions.Def_CannonFloydParry import Definitions.Def_CannonFloydParry_Trees import Definitions.Def_CannonFloydParry_TreeDiagrams import Mathlib
namespace CannonFloydParry
theorem isReduced_represents_unique {f : UI ≃o UI} {d₁ d₂ : TreeDiagram}
(h₁ : IsReduced d₁) (hr₁ : Represents d₁ f)
(h₂ : IsReduced d₂) (hr₂ : Represents d₂ f) :
d₁ = d₂ := by
sorry
end CannonFloydParry
Read-back
What the Lean code literally says, in plain math · claude-opus-5
Read-back
The ambient group
Let be the closed unit interval of real numbers, regarded as an ordered set with the order it inherits from .
Let denote the set of order-isomorphisms : bijections such that . This is a group under composition, with
Every element of automatically satisfies and , since an order-isomorphism carries the least element to the least element and the greatest to the greatest.
Dyadic numbers, and the generating property
A real number is dyadic if for some integer and some natural number . (Since is allowed, every integer is dyadic; may be negative, so dyadic numbers are not confined to .)
Say that has property if there exists a finite set , every element of which is dyadic, such that:
for all with and , there exist an integer and a real number such that
Three points about property as stated. The exponent ranges over the integers, so the slope is a positive integer power of (possibly a negative power), never an arbitrary positive real; the intercept is an arbitrary real. The finite set is only required to consist of dyadic reals — it is not required to be contained in , nor to contain or , and it may be empty. The interval avoided is the open interval , while the affine identity is asserted on the closed interval .
Let be the subgroup generated by the set , that is, the smallest subgroup of containing every with property (equivalently, the intersection of all such subgroups). So "" means: is a finite product of elements having property and of inverses of such elements. The statement below does not assume that the set of elements with property is already closed under composition or inversion; is its group closure whether or not that is so.
Finite binary trees
A tree is either a single leaf, or a node carrying an ordered pair of trees (its left and right subtrees). These are finite rooted ordered binary trees in which every internal node has exactly two children.
The leaf count is defined by and . Thus for every tree, and exactly when is a single leaf.
The leaves of a tree are numbered from left to right, in the usual depth-first left-to-right order.
The marks of a tree
Assign real intervals to the nodes of by bisection: the root gets , and a node holding gives its left subtree and its right subtree . The intervals assigned to the leaves, read left to right, partition into consecutive standard dyadic intervals of the form .
The marks of , written , are the endpoints of that partition listed in increasing order:
where and is the interval of the -th leaf. This is a list (an ordered, finite sequence), of length ; it always has at least the two entries and , and for the single leaf it is exactly .
The caret predicate
For a tree and a natural number , define a truth value by the following recursion on . For the single leaf, is false for every . For :
- if , then ;
- otherwise, if , then ;
- otherwise (the remaining case is exactly , i.e. is the index of the rightmost leaf of ), is true if both and are single leaves, and false otherwise.
The first two guards are mutually exclusive — and cannot both hold — so the three clauses are genuinely a case split with no ambiguity, and the third clause governs precisely the single index .
What this computes is:
Equivalently: has a node both of whose children are leaves, and those two leaves are the -th and -st leaves of . In particular is false whenever — so it is false at every index at or beyond the last leaf, and false for every when is a single leaf. (This equivalence was checked exhaustively against a direct implementation for all trees of depth at most , which includes trees with up to leaves, at every index up to .)
Tree diagrams
A tree diagram consists of three pieces of data: a tree , a tree , and a proof of the assertion . The third component is a proof of a proposition and carries no further information: two tree diagrams are equal if and only if their two trees agree,
where equality of trees is equality of the tree shapes as combinatorial objects. So a tree diagram is, in effect, an ordered pair of trees with the same number of leaves.
Extension to the line
For , let be
This is an order-isomorphism of (it is well defined and order-preserving across the seams because and ).
What it means for a diagram to represent a map
Write and . The diagram represents when all three of the following hold.
-
.
-
(Affine on the pieces of the domain tree.) For every with — that is, for each pair of consecutive entries of — there exist real numbers and such that
The numbers are arbitrary reals: nothing here requires , nor that be a power of , nor that the be related to one another. The condition is imposed only on consecutive pairs of marks, and says nothing directly about non-adjacent pairs. The interval is the closed interval , so consecutive conditions overlap at the shared endpoint.
- (The marks are carried to the marks, in order.) Applying entrywise to the list yields the list exactly:
Being an equality of lists, this forces — hence , which the diagram already carries as its third component — and forces for every index separately, in the same order.
What it means for a diagram to be reduced
The diagram is reduced when, for every natural number , it is not the case that both and are true. In words: there is no index at which the domain tree and the range tree both have a node whose two children are exactly their -th and -st leaves.
The quantifier runs over all natural numbers , including those at or beyond the last leaf, where both caret predicates are false anyway, so those indices impose nothing. The condition permits the domain tree to have such a node at one index and the range tree to have one at a different index; only coincidence of indices is forbidden.
The assertion
Let be any order-isomorphism of , and let and be any tree diagrams. Suppose that is reduced and represents , and that is reduced and represents . Then .
Unfolded completely: for every order-isomorphism and all trees with and , if
- there is no with and both true, and
- lies in the subgroup , and is affine on each interval between consecutive marks of , and carries the list of marks of entrywise onto the list of marks of , and
- there is no with and both true, and
- lies in , and is affine on each interval between consecutive marks of , and carries the list of marks of entrywise onto the list of marks of ,
then and .
Scope, quantifiers and edge cases
-
The map and the two diagrams are universally quantified; they are the only variables. There are no side conditions of a typeclass or structural nature beyond those spelled out above.
-
The clause "" occurs inside each of the two representation hypotheses, so it is assumed twice with identical content; it is the same in both.
-
The hypotheses are jointly satisfiable, so the statement is not vacuous. Taking to be the identity map of and to be the diagram whose two trees are both a single leaf: the identity lies in (it is the neutral element of a subgroup); the marks of a single leaf are , on which the identity is affine with , ; the identity carries to ; and the caret predicate of a single leaf is false everywhere, so the diagram is reduced. All four hypotheses hold simultaneously. (Verified by elaboration.)
-
The conclusion is equality of the diagrams, which as noted above is exactly equality of both underlying trees. It is not merely equality of leaf counts, nor equality of the induced piecewise-linear maps, nor equality up to some notion of isomorphism of diagrams.
-
The statement asserts uniqueness only: at most one reduced diagram represents a given . It makes no claim that any reduced diagram representing exists, and no claim about which (or which ) are representable at all. Correspondingly, if for some no reduced representing diagram exists, the statement holds for that with nothing to say.
-
If the domain tree of a diagram is a single leaf, then its leaf count is , so by the diagram's own third component the range tree also has leaf count and is therefore also a single leaf; such a diagram is automatically reduced.
-
Nothing in the representation condition refers to the marks of the range tree except as the target list in clause 3; in particular the affineness in clause 2 is imposed relative to the subdivision coming from the domain tree only.
-
The notion of "reduced" used here is the one defined above — absence of a common index at which both trees have a node with two leaf children. No further minimality, irreducibility or normal-form condition on the diagram is assumed.
Confirmed by the mission captain (proposal self-audit).