Rooted Vertex Reconstruction

Abstract

Equal branch codes reconstruct actual rooted vertices and internal child edges.

Definition 1.1 (Original descendant vertices).

$$\begin{array}{c}u\mathrm{universe},\forall Y:{\mathrm{Type}}_u,f:Y\to Y,r:Y,\\ \mathrm{Descendant}\left(f,r\right):=\{x:Y\mid \mathrm{ReflTransGen}\left(\mathrm{TransientChild}\left(f\right),x,r\right)\}\end{array}$$

Formalization. D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.Descendant (✓ std3).

Source. Repository-derived.

Commentary.

The carrier is a subtype of the original state space. The root is included by the reflexive path. TransientChild is the existing nonperiodic-child relation, directed toward the parent; val denotes subtype projection.

Definition 1.2 (Root-preserving vertex equivalence).

$$\begin{array}{c}u,v\mathrm{universes},\\ \forall Y:{\mathrm{Type}}_u,Z:{\mathrm{Type}}_v,\\ \forall f:Y\to Y,g:Z\to Z,r:Y,s:Z,\\ \mathrm{RootedVertexEquiv}(f,g,r,s)\mathrm{fields}:\\ \mathrm{equiv}:\mathrm{Equiv}\left(\mathrm{Descendant}\left(f,r\right),\mathrm{Descendant}\left(g,s\right)\right),\\ \mathrm{rootEq}:\mathrm{equiv}\left(⟨r,\mathrm{refl}⟩\right)=⟨s,\mathrm{refl}⟩,\\ \mathrm{childIff}:\forall a,b:\mathrm{Descendant}\left(f,r\right),\mathrm{TransientChild}\left(f,\mathrm{val}\left(a\right),\mathrm{val}\left(b\right)\right)⟺\mathrm{TransientChild}\left(g,\mathrm{val}\left(\mathrm{equiv}\left(a\right)\right),\mathrm{val}\left(\mathrm{equiv}\left(b\right)\right)\right)\end{array}$$

Formalization. D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.RootedVertexEquiv (✓ std3).

Source. Repository-derived.

Commentary.

The displayed equiv, rootEq, and childIff denote the Lean fields equiv, root_eq, and child_iff. The equivalence includes both inverse laws. This definition requires no finiteness instances; finiteness is used by the reconstruction theorem.

Definition 1.3 (Root and disjoint child subtrees).

$$\begin{array}{c}u\mathrm{universe},\forall Y:{\mathrm{Type}}_u,[\mathrm{Finite}\left(Y\right)],\\ \forall f:Y\to Y,r:Y,\\ p:=\mathrm{descendantPartition}\left(f,r\right):\mathrm{Equiv}\left(\mathrm{Option}\left({\mathrm{Sigma}}_{c:\{c:Y\mid \mathrm{TransientChild}\left(f,c,r\right)\}}\mathrm{Descendant}\left(f,\mathrm{val}\left(c\right)\right)\right),\mathrm{Descendant}\left(f,r\right)\right),\\ p\left(\mathrm{none}\right)=⟨r,\mathrm{refl}⟩,\\ \forall c:\{c:Y\mid \mathrm{TransientChild}\left(f,c,r\right)\},x:\mathrm{Descendant}\left(f,\mathrm{val}\left(c\right)\right),\mathrm{val}\left(p\left(\mathrm{some}\left(⟨c,x⟩\right)\right)\right)=\mathrm{val}\left(x\right),\\ \forall a:\mathrm{Option}\left({\mathrm{Sigma}}_{c:\{c:Y\mid \mathrm{TransientChild}\left(f,c,r\right)\}}\mathrm{Descendant}\left(f,\mathrm{val}\left(c\right)\right)\right),\mathrm{inverse}\left(p,p\left(a\right)\right)=a,\\ \forall x:\mathrm{Descendant}\left(f,r\right),p\left(\mathrm{inverse}\left(p,x\right)\right)=x\end{array}$$

Formalization. D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.descendantPartition (✓ std3).

Source. Repository-derived.

Commentary.

The Option value none denotes the root. A some value carries an actual immediate child and an original vertex below that child. Deterministic parents make paths comparable; well-foundedness excludes a return to the root and forces the immediate child to be unique. The resulting bijection supplies the inverse used in reconstruction.

Theorem 1.4 (Equal branch codes reconstruct rooted vertices).

$$\begin{array}{c}u,v\mathrm{universes},\\ \forall Y:{\mathrm{Type}}_u,Z:{\mathrm{Type}}_v,\\ [\mathrm{Fintype}\left(Y\right)],[\mathrm{Fintype}\left(Z\right)],\\ \forall f:Y\to Y,g:Z\to Z,r:Y,s:Z,\\ \mathrm{branchCode}\left(f,r\right)=\mathrm{branchCode}\left(g,s\right)⟹\\ \exists e:\mathrm{Equiv}\left(\mathrm{Descendant}\left(f,r\right),\mathrm{Descendant}\left(g,s\right)\right),\\ e\left(⟨r,\mathrm{refl}⟩\right)=⟨s,\mathrm{refl}⟩\wedge \\ (\forall a,b:\mathrm{Descendant}\left(f,r\right),\mathrm{TransientChild}\left(f,\mathrm{val}\left(a\right),\mathrm{val}\left(b\right)\right)⟺\mathrm{TransientChild}\left(g,\mathrm{val}\left(e\left(a\right)\right),\mathrm{val}\left(e\left(b\right)\right)\right))\end{array}$$

Proof. Machine-checked in Lean as D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.rooted_vertex_equiv_of_branch_code_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

RootedVertexEquiv stores precisely the displayed equivalence, root equality, and child-relation iff in its equiv, root_eq, and child_iff fields. The theorem asserts that this structure is nonempty. The two universes are independent, and no equality of ambient cardinalities is assumed.

Equality of encoded child multisets matches occurrences with their full multiplicities. Well-founded recursion constructs the child equivalences. The actual partition inverse, the dependent sum of those equivalences, and the target partition form the vertex equivalence. The edge proof includes both internal subtree edges and edges from child roots to the root.

An arbitrary root may be transient, and its outgoing update may leave this carrier. The result asserts only the displayed internal child relation. The converse classification, cycle and component gluing, cardinal-depth saturation, and the compatible-family inverse are separate obligations.

Theorem 1.5 (Recursive matching reconstructs the same vertices).

$$\begin{array}{c}u,v\mathrm{universes},\\ \forall Y:{\mathrm{Type}}_u,Z:{\mathrm{Type}}_v,\\ [\mathrm{Fintype}\left(Y\right)],[\mathrm{Fintype}\left(Z\right)],\\ \forall f:Y\to Y,g:Z\to Z,r:Y,s:Z,\\ \mathrm{RootedTransientTreeIsomorphic}\left(f,g,r,s\right)⟹\\ \exists e:\mathrm{Equiv}\left(\mathrm{Descendant}\left(f,r\right),\mathrm{Descendant}\left(g,s\right)\right),\\ e\left(⟨r,\mathrm{refl}⟩\right)=⟨s,\mathrm{refl}⟩\wedge \\ (\forall a,b:\mathrm{Descendant}\left(f,r\right),\mathrm{TransientChild}\left(f,\mathrm{val}\left(a\right),\mathrm{val}\left(b\right)\right)⟺\mathrm{TransientChild}\left(g,\mathrm{val}\left(e\left(a\right)\right),\mathrm{val}\left(e\left(b\right)\right)\right))\end{array}$$

Proof. Machine-checked in Lean as D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.rooted_vertex_equiv_of_recursive_isomorphism (✓ std3). ∎

Source. Repository-derived.

Commentary.

The existing recursive Multiset.Rel predicate gives equal branch codes by the frozen classifier, so the same reconstruction applies.

References

• Truth anchor: D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.Descendant
• Truth anchor: D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.RootedVertexEquiv
• Truth anchor: D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.descendantPartition
• Truth anchor: D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.rooted_vertex_equiv_of_branch_code_eq
• Truth anchor: D5/S1/FixedPoints/TransientTrees/RootedVertexReconstruction.rooted_vertex_equiv_of_recursive_isomorphism
• Dependency: D5/S1/FixedPoints/RootedTransientTreeClassification