Hepp trees: carrier, canonicalization, automorphism group, markings (node D-hepp)

Paper: D-hepp — Hepp trees, markings, the automorphism group

Stable Hepp-tree carrier and the Hepp-specific data of paper Definition 5.1: branching vertices, leaves, dyadic markings, leaf multiplicities.

• PlaneTree — plane rooted trees (nested inductive through List); size, leafCount, isValid (no unary vertices), injective serialization key, canonical order-forgotten form canon, and the automorphism-count formula autCard (run factorials on canonically sorted children × children's counts).
• Vertices are position paths (VPos); the automorphism group Aut t is the subgroup of vertex permutations commuting with the total parent map, acting on markings with orbit–stabilizer (card_orbit_mul_card_autMarked).
• BranchNodes, Leaves, HeppMarking, Multiplicities — Def 5.1 data.
• card_aut_eq_autCard — the D-hepp cross-check tying both descriptions.

Implementation note: children are sorted with mathlib's structurally recursive List.insertionSort instead of List.mergeSort, because mergeSort is defined by well-founded recursion and does not reduce in the kernel; the carrier needs decide/rfl to evaluate autCard. All helpers below are structurally recursive.

inductive Anderson4D.PlaneTree : Type

Plane rooted tree; node [] is a leaf. Carrier for Hepp trees (paper Def 5.1); Hepp validity (branching ⇒ ≥ 2 children) is the separate predicate isValid, and markings/multiplicities are separate data.

• node : List PlaneTree → PlaneTree

def Anderson4D.PlaneTree.size : PlaneTree → ℕ

Number of vertices.

Equations

• (Anderson4D.PlaneTree.node cs).size = 1 + Anderson4D.PlaneTree.sizeList cs

def Anderson4D.PlaneTree.sizeList : List PlaneTree → ℕ

Companion of size: total vertex count of a forest.

Equations

• Anderson4D.PlaneTree.sizeList [] = 0
• Anderson4D.PlaneTree.sizeList (c :: cs) = c.size + Anderson4D.PlaneTree.sizeList cs

theorem Anderson4D.PlaneTree.sizeList_eq_map (cs : List PlaneTree) : sizeList cs = (List.map size cs).sum

sizeList is the sum of the children's sizes.

def Anderson4D.PlaneTree.leafCount : PlaneTree → ℕ

Number of leaves; a bare node [] counts as one leaf. (Children's leaf counts are all ≥ 1, so the max 1 only affects the leaf case.)

Equations

• (Anderson4D.PlaneTree.node cs).leafCount = max 1 (Anderson4D.PlaneTree.leafCountList cs)

def Anderson4D.PlaneTree.leafCountList : List PlaneTree → ℕ

Companion of leafCount: total leaf count of a forest.

Equations

• Anderson4D.PlaneTree.leafCountList [] = 0
• Anderson4D.PlaneTree.leafCountList (c :: cs) = c.leafCount + Anderson4D.PlaneTree.leafCountList cs

theorem Anderson4D.PlaneTree.leafCountList_eq_map (cs : List PlaneTree) : leafCountList cs = (List.map leafCount cs).sum

leafCountList is the sum of the children's leaf counts.

def Anderson4D.PlaneTree.isValid : PlaneTree → Bool

Hepp validity: no internal vertex has exactly one child.

Equations

• (Anderson4D.PlaneTree.node cs).isValid = (cs.length != 1 && Anderson4D.PlaneTree.isValidList cs)

def Anderson4D.PlaneTree.isValidList : List PlaneTree → Bool

Companion of isValid: validity of every tree in a forest.

Equations

• Anderson4D.PlaneTree.isValidList [] = true
• Anderson4D.PlaneTree.isValidList (c :: cs) = (c.isValid && Anderson4D.PlaneTree.isValidList cs)

theorem Anderson4D.PlaneTree.isValidList_eq_map (cs : List PlaneTree) : isValidList cs = (List.map isValid cs).all id

isValidList is the conjunction of the children's validities.

def Anderson4D.PlaneTree.key : PlaneTree → List ℕ

Injective serialization (balanced-parentheses encoding): 0 opens a node and 1 closes it. Injectivity is proved below using the stack decoder.

Equations

• (Anderson4D.PlaneTree.node cs).key = 0 :: (Anderson4D.PlaneTree.keyList cs ++ [1])

def Anderson4D.PlaneTree.keyList : List PlaneTree → List ℕ

Companion of key: concatenated keys of a forest.

Equations

• Anderson4D.PlaneTree.keyList [] = []
• Anderson4D.PlaneTree.keyList (c :: cs) = c.key ++ Anderson4D.PlaneTree.keyList cs

theorem Anderson4D.PlaneTree.keyList_eq_map (cs : List PlaneTree) : keyList cs = (List.map key cs).flatten

keyList is the flattened list of the children's keys.

def Anderson4D.PlaneTree.lexLe : List ℕ → List ℕ → Bool

Lexicographic ≤ on serialization keys, as a Bool comparator.

Equations

• Anderson4D.PlaneTree.lexLe [] x✝ = true
• Anderson4D.PlaneTree.lexLe (head :: tail) [] = false
• Anderson4D.PlaneTree.lexLe (a :: as) (b :: bs) = if a < b then true else if b < a then false else Anderson4D.PlaneTree.lexLe as bs

def Anderson4D.PlaneTree.KeyLe (a b : PlaneTree) : Prop

Key-lexicographic comparison of trees (a decidable total preorder), the sorting relation for canonicalization.

Equations

• a.KeyLe b = (Anderson4D.PlaneTree.lexLe a.key b.key = true)

@[implicit_reducible]

instance Anderson4D.PlaneTree.instDecidableRelKeyLe : DecidableRel KeyLe

Equations

• a.instDecidableRelKeyLe b = Anderson4D.PlaneTree.instDecidableRelKeyLe._aux_1 a b

def Anderson4D.PlaneTree.canon : PlaneTree → PlaneTree

Canonical (order-forgotten) representative: recursively canonicalize children, then sort them by key. Two plane trees represent the same unordered rooted tree iff their canonical forms are equal.

Equations

• (Anderson4D.PlaneTree.node cs).canon = Anderson4D.PlaneTree.node (List.insertionSort Anderson4D.PlaneTree.KeyLe (Anderson4D.PlaneTree.canonList cs))

def Anderson4D.PlaneTree.canonList : List PlaneTree → List PlaneTree

Companion of canon: canonicalize every tree in a forest.

Equations

• Anderson4D.PlaneTree.canonList [] = []
• Anderson4D.PlaneTree.canonList (c :: cs) = c.canon :: Anderson4D.PlaneTree.canonList cs

theorem Anderson4D.PlaneTree.canonList_eq_map (cs : List PlaneTree) : canonList cs = List.map canon cs

canonList is List.map canon.

def Anderson4D.PlaneTree.runsProdFactorial : List PlaneTree → ℕ

Product of (run length)! over maximal runs of key-equal adjacent elements (intended for canonicalized, i.e. sorted, children lists).

Equations

• Anderson4D.PlaneTree.runsProdFactorial [] = 1
• Anderson4D.PlaneTree.runsProdFactorial (c :: cs) = Anderson4D.PlaneTree.runsProdFactorial.go c 1 cs

def Anderson4D.PlaneTree.runsProdFactorial.go : PlaneTree → ℕ → List PlaneTree → ℕ

Tail of runsProdFactorial: go c k ds scans ds with current run representative c of length k.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.PlaneTree.runsProdFactorial.go a✝¹ a✝ [] = a✝.factorial

def Anderson4D.PlaneTree.autCard : PlaneTree → ℕ

Order of the automorphism group of the unordered rooted tree represented by a plane tree: permutations of iso-equal children (run factorials on the canonicalized children) times the children's own automorphism counts (Prop 5.6's |Aut(T)|). Cross-checked against the permutation-subgroup order in card_aut_eq_autCard.

Equations

• One or more equations did not get rendered due to their size.

def Anderson4D.PlaneTree.autCardList : List PlaneTree → ℕ

Companion of autCard: product of the automorphism counts of a forest.

Equations

• Anderson4D.PlaneTree.autCardList [] = 1
• Anderson4D.PlaneTree.autCardList (c :: cs) = c.autCard * Anderson4D.PlaneTree.autCardList cs

theorem Anderson4D.PlaneTree.autCardList_eq_map (cs : List PlaneTree) : autCardList cs = (List.map autCard cs).prod

autCardList is the product of the children's automorphism counts.

Basic examples and compiled-evaluation sanity checks

def Anderson4D.PlaneTree.leaf : PlaneTree

A leaf.

Equations

• Anderson4D.PlaneTree.leaf = Anderson4D.PlaneTree.node []

def Anderson4D.PlaneTree.cherry : PlaneTree

A cherry: two leaves. |Aut| = 2.

Equations

• Anderson4D.PlaneTree.cherry = Anderson4D.PlaneTree.node [Anderson4D.PlaneTree.leaf, Anderson4D.PlaneTree.leaf]

Positions (vertex addresses)

@[reducible, inline]

abbrev Anderson4D.PlaneTree.Pos : Type

A vertex address: the path of child indices from the root.

Equations

• Anderson4D.PlaneTree.Pos = List ℕ

def Anderson4D.PlaneTree.isPos : PlaneTree → Pos → Bool

Validity of a position in a tree (Bool-valued, kernel-reducible).

Equations

• x✝.isPos [] = true
• (Anderson4D.PlaneTree.node cs).isPos (i :: p) = if h : i < cs.length then cs[i].isPos p else false

def Anderson4D.PlaneTree.IsPos (t : PlaneTree) (p : Pos) : Prop

Position validity, Prop-valued.

Equations

• t.IsPos p = (t.isPos p = true)

@[implicit_reducible]

instance Anderson4D.PlaneTree.instDecidablePredPosIsPos (t : PlaneTree) : DecidablePred t.IsPos

Equations

• t.instDecidablePredPosIsPos p = Anderson4D.PlaneTree.instDecidablePredPosIsPos._aux_1 t p

theorem Anderson4D.PlaneTree.isPos_nil (t : PlaneTree) : t.IsPos []

The root position is valid in every tree.

theorem Anderson4D.PlaneTree.isPos_cons_iff {cs : List PlaneTree} {i : ℕ} {p : Pos} : (node cs).IsPos (i :: p) ↔ ∃ (h : i < cs.length), cs[i].IsPos p

Unfolding IsPos along one step into child i.

theorem Anderson4D.PlaneTree.IsPos.dropLast {t : PlaneTree} {p : Pos} (h : t.IsPos p) : t.IsPos (List.dropLast p)

The parent of a valid vertex is valid; the root maps to itself.

def Anderson4D.PlaneTree.positions : PlaneTree → List Pos

All valid positions of t, root first.

Equations

• One or more equations did not get rendered due to their size.

def Anderson4D.PlaneTree.positionsList : List PlaneTree → List (List Pos)

Companion of positions for the children list.

Equations

• Anderson4D.PlaneTree.positionsList [] = []
• Anderson4D.PlaneTree.positionsList (c :: cs) = c.positions :: Anderson4D.PlaneTree.positionsList cs

theorem Anderson4D.PlaneTree.positionsList_eq_map (cs : List PlaneTree) : positionsList cs = List.map positions cs

positionsList is List.map positions.

theorem Anderson4D.PlaneTree.mem_positions (t : PlaneTree) (p : Pos) : p ∈ t.positions ↔ t.IsPos p

positions enumerates exactly the valid positions.

@[reducible, inline]

abbrev Anderson4D.PlaneTree.VPos (t : PlaneTree) : Type

The (finite) vertex set of t: valid positions.

Equations

• t.VPos = { p : Anderson4D.PlaneTree.Pos // t.IsPos p }

@[implicit_reducible]

instance Anderson4D.PlaneTree.instFintypeVPos (t : PlaneTree) : Fintype t.VPos

Equations

• t.instFintypeVPos = Fintype.subtype t.positions.toFinset ⋯

def Anderson4D.PlaneTree.rootV (t : PlaneTree) : t.VPos

The root vertex.

Equations

• t.rootV = ⟨[], ⋯⟩

def Anderson4D.PlaneTree.parentV {t : PlaneTree} (v : t.VPos) : t.VPos

Total parent map on vertices; the root is its own parent.

Equations

• Anderson4D.PlaneTree.parentV v = ⟨List.dropLast ↑v, ⋯⟩

The automorphism group

A vertex permutation is an automorphism of the unordered rooted tree iff it commutes with the total parent map (a classical, HEq-free characterization).

def Anderson4D.PlaneTree.IsAut (t : PlaneTree) (e : Equiv.Perm t.VPos) : Prop

A vertex permutation is an automorphism of the unordered rooted tree iff it commutes with the parent map.

Equations

• t.IsAut e = ∀ (v : t.VPos), e (Anderson4D.PlaneTree.parentV v) = Anderson4D.PlaneTree.parentV (e v)

@[implicit_reducible]

instance Anderson4D.PlaneTree.instDecidablePredPermVPosIsAut (t : PlaneTree) : DecidablePred t.IsAut

Equations

• t.instDecidablePredPermVPosIsAut e = Anderson4D.PlaneTree.instDecidablePredPermVPosIsAut._aux_1 t e

def Anderson4D.PlaneTree.autSubgroup (t : PlaneTree) : Subgroup (Equiv.Perm t.VPos)

Automorphisms of the unordered rooted tree presented by t, as a subgroup of the vertex permutations.

Equations

• t.autSubgroup = { carrier := {e : Equiv.Perm t.VPos | t.IsAut e}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[implicit_reducible]

instance Anderson4D.PlaneTree.instDecidablePredPermVPosMemSubgroupAutSubgroup (t : PlaneTree) : DecidablePred fun (x : Equiv.Perm t.VPos) => x ∈ t.autSubgroup

Equations

• t.instDecidablePredPermVPosMemSubgroupAutSubgroup e = decidable_of_iff (t.IsAut e) ⋯

@[reducible, inline]

abbrev Anderson4D.PlaneTree.Aut (t : PlaneTree) : Type

The automorphism group of (the unordered tree presented by) t.

Equations

• t.Aut = ↥t.autSubgroup

theorem Anderson4D.PlaneTree.apply_root_eq {t : PlaneTree} (g : t.Aut) : ↑g t.rootV = t.rootV

Every automorphism fixes the root (automatic from parent-commutation).

Markings and the action of Aut

@[reducible, inline]

abbrev Anderson4D.PlaneTree.Marking (t : PlaneTree) : Type

A plain marking: one natural number per vertex (the raw carrier on which Aut t acts; the Def 5.1 constraints are bundled in HeppMarking).

Equations

• t.Marking = (t.VPos → ℕ)

@[implicit_reducible]

instance Anderson4D.PlaneTree.instMulActionAutMarking (t : PlaneTree) : MulAction t.Aut t.Marking

Aut t acts on markings by precomposition with the inverse vertex transport (the position transport is just g.1 : Equiv.Perm (VPos t)).

Equations

• t.instMulActionAutMarking = { smul := fun (g : t.Aut) (N : t.Marking) (v : t.VPos) => N (↑g⁻¹ v), mul_smul := ⋯, one_smul := ⋯ }

theorem Anderson4D.PlaneTree.smul_marking_apply {t : PlaneTree} (g : t.Aut) (N : t.Marking) (v : t.VPos) : (g • N) v = N (↑g⁻¹ v)

Unfolding lemma for the action on markings.

@[reducible, inline]

abbrev Anderson4D.PlaneTree.AutMarked (t : PlaneTree) (N : t.Marking) : Subgroup t.Aut

Automorphisms of the marked tree (T, N) = the marking stabilizer (paper's Aut(T, N) in Prop 5.6).

Equations

• t.AutMarked N = MulAction.stabilizer t.Aut N

@[implicit_reducible]

instance Anderson4D.PlaneTree.instDecidablePredAutMemSubgroupAutMarked (t : PlaneTree) (N : t.Marking) : DecidablePred fun (x : t.Aut) => x ∈ t.AutMarked N

Equations

• t.instDecidablePredAutMemSubgroupAutMarked N g = decidable_of_iff (g • N = N) ⋯

@[implicit_reducible]

instance Anderson4D.PlaneTree.instFintypeElemMarkingOrbitAut (t : PlaneTree) (N : t.Marking) : Fintype ↑(MulAction.orbit t.Aut N)

Equations

• t.instFintypeElemMarkingOrbitAut N = Fintype.ofFinset (Finset.image (fun (g : t.Aut) => g • N) Finset.univ) ⋯

theorem Anderson4D.PlaneTree.card_orbit_mul_card_autMarked (t : PlaneTree) (N : t.Marking) : (MulAction.orbit t.Aut N).toFinset.card * Fintype.card ↥(t.AutMarked N) = Fintype.card t.Aut

Orbit–stabilizer for marked trees (Prop 5.6 counting step): #(orbit of N) · |Aut(T, N)| = |Aut(T)|.

Sanity checks on the cherry

def Anderson4D.PlaneTree.testMark : cherry.Marking

A marking separating the two leaves of the cherry (sanity checks only).

Equations

• Anderson4D.PlaneTree.testMark v = if ↑v = [0] then 1 else 0

Hepp data (paper Def 5.1): branching vertices, leaves, markings,

multiplicities

def Anderson4D.PlaneTree.childCount : PlaneTree → Pos → ℕ

Number of children of the vertex at position p (0 if p is invalid); Bool-free companion of isPos, kernel-reducible.

Equations

• (Anderson4D.PlaneTree.node cs).childCount [] = cs.length
• (Anderson4D.PlaneTree.node cs).childCount (i :: p) = if h : i < cs.length then cs[i].childCount p else 0

def Anderson4D.PlaneTree.BranchNodes (t : PlaneTree) : Finset t.VPos

Branching vertices: at least two children (paper Def 5.1's branching nodes; in a Hepp-valid tree every internal vertex is branching).

Equations

• t.BranchNodes = {v : t.VPos | 2 ≤ t.childCount ↑v}

def Anderson4D.PlaneTree.Leaves (t : PlaneTree) : Finset t.VPos

Leaves: childless vertices.

Equations

• t.Leaves = {v : t.VPos | t.childCount ↑v = 0}

structure Anderson4D.PlaneTree.HeppMarking (t : PlaneTree) : Type

A Hepp marking on t (paper Def 5.1): dyadic scales N_n = 2 ^ Nexp n attached to the branching vertices, with N_n ≥ 2 and strictly increasing toward the root (N_{n⁺} > N_n for the parent n⁺). The exponent function Nexp is stored as a total function on all vertices; its values at non-branching vertices are junk (unconstrained), and both constraints quantify over BranchNodes t only. Note that in a Hepp-valid tree the parent of any vertex has ≥ 2 children, so parent_gt only ever inspects Nexp at branching vertices.

• Nexp : t.VPos → ℕ

  Exponent of the dyadic scale: the paper's N_n is 2 ^ Nexp n.

• pos (v : t.VPos) : v ∈ t.BranchNodes → 1 ≤ self.Nexp v

  Scales are dyadic with exponent ≥ 1, i.e. N_n ∈ {2, 4, 8, …}.

• parent_gt (v : t.VPos) : v ∈ t.BranchNodes → v ≠ t.rootV → self.Nexp (parentV v) > self.Nexp v

  Strict monotonicity toward the root: the parent's scale is larger.

structure Anderson4D.PlaneTree.Multiplicities (t : PlaneTree) : Type

Leaf multiplicities on t (paper Def 5.1): m v ≥ 2 at every leaf; values at non-leaf vertices are junk (unconstrained).

• m : t.VPos → ℕ

  The multiplicity of each leaf.

• two_le (v : t.VPos) : v ∈ t.Leaves → 2 ≤ self.m v

  Every leaf occurs with multiplicity at least two.

Proof toolkit for the D-hepp cross-check

Key injectivity (stack decoder), order properties of KeyLe, the vertex calculus of node trees (childV), tree isomorphisms Iso as parent-commuting vertex bijections, the graft/split equivalence for nodes, permutations of fibers of a classification, and run-length counting on canonically sorted lists. All of it feeds card_aut_eq_autCard.

Key injectivity via a stack decoder

def Anderson4D.PlaneTree.dec : List ℕ → List (List PlaneTree) → List (List PlaneTree)

Stack decoder inverting key: token 0 opens a frame, token 1 closes the top frame into the frame below (children are collected in reverse order).

Equations

• Anderson4D.PlaneTree.dec [] x✝ = x✝
• Anderson4D.PlaneTree.dec (0 :: xs) x✝ = Anderson4D.PlaneTree.dec xs ([] :: x✝)
• Anderson4D.PlaneTree.dec (1 :: xs) (ts :: us :: st) = Anderson4D.PlaneTree.dec xs ((Anderson4D.PlaneTree.node ts.reverse :: us) :: st)
• Anderson4D.PlaneTree.dec (head :: xs) x✝ = Anderson4D.PlaneTree.dec xs x✝

theorem Anderson4D.PlaneTree.dec_key_append (t : PlaneTree) (xs : List ℕ) (acc : List PlaneTree) (st : List (List PlaneTree)) : dec (t.key ++ xs) (acc :: st) = dec xs ((t :: acc) :: st)

Running the decoder over key t pushes t onto the top frame.

theorem Anderson4D.PlaneTree.dec_keyList_append (cs : List PlaneTree) (xs : List ℕ) (acc : List PlaneTree) (st : List (List PlaneTree)) : dec (keyList cs ++ xs) (acc :: st) = dec xs ((cs.reverse ++ acc) :: st)

Companion of dec_key_append for forests.

theorem Anderson4D.PlaneTree.key_injective : Function.Injective key

The serialization key is injective.

@[implicit_reducible]

instance Anderson4D.PlaneTree.instDecidableEq : DecidableEq PlaneTree

Equations

• a.instDecidableEq b = decidable_of_iff (a.key = b.key) ⋯

The lexicographic comparator is a total preorder, antisymmetric on keys

theorem Anderson4D.PlaneTree.lexLe_cons_lt {a b : ℕ} {as bs : List ℕ} (h : a < b) : lexLe (a :: as) (b :: bs) = true

theorem Anderson4D.PlaneTree.lexLe_cons_gt {a b : ℕ} {as bs : List ℕ} (h : b < a) : lexLe (a :: as) (b :: bs) = false

theorem Anderson4D.PlaneTree.lexLe_cons_eq {a : ℕ} {as bs : List ℕ} : lexLe (a :: as) (a :: bs) = lexLe as bs

theorem Anderson4D.PlaneTree.lexLe_total (a b : List ℕ) : lexLe a b = true ∨ lexLe b a = true

theorem Anderson4D.PlaneTree.lexLe_trans (a b c : List ℕ) : lexLe a b = true → lexLe b c = true → lexLe a c = true

theorem Anderson4D.PlaneTree.lexLe_antisymm (a b : List ℕ) : lexLe a b = true → lexLe b a = true → a = b

instance Anderson4D.PlaneTree.instTotalKeyLe : Std.Total KeyLe

instance Anderson4D.PlaneTree.instIsTransKeyLe : IsTrans PlaneTree KeyLe

instance Anderson4D.PlaneTree.instAntisymmKeyLe : Std.Antisymm KeyLe

theorem Anderson4D.PlaneTree.key_notMem_map_of_pairwise {c d : PlaneTree} {ds : List PlaneTree} (h : List.Pairwise KeyLe (c :: d :: ds)) (hne : c.key ≠ d.key) : c.key ∉ List.map key (d :: ds)

In a KeyLe-pairwise list c :: d :: ds with key c ≠ key d, the key of c occurs nowhere from d on.

Vertices of a node: root and child embeddings

theorem Anderson4D.PlaneTree.isPos_cons_lt {cs : List PlaneTree} {i : ℕ} {p : Pos} (h : (node cs).IsPos (i :: p)) : i < cs.length

theorem Anderson4D.PlaneTree.isPos_cons_tail {cs : List PlaneTree} {i : ℕ} {p : Pos} (h : (node cs).IsPos (i :: p)) : (cs.get ⟨i, ⋯⟩).IsPos p

def Anderson4D.PlaneTree.childV {cs : List PlaneTree} (i : Fin cs.length) (v : (cs.get i).VPos) : (node cs).VPos

The vertex of node cs at position i :: v inside child i.

Equations

• Anderson4D.PlaneTree.childV i v = ⟨↑i :: ↑v, ⋯⟩

@[simp]

theorem Anderson4D.PlaneTree.childV_val {cs : List PlaneTree} (i : Fin cs.length) (v : (cs.get i).VPos) : ↑(childV i v) = ↑i :: ↑v

theorem Anderson4D.PlaneTree.childV_ne_root {cs : List PlaneTree} (i : Fin cs.length) (v : (cs.get i).VPos) : childV i v ≠ (node cs).rootV

theorem Anderson4D.PlaneTree.childV_inj_idx {cs : List PlaneTree} {i j : Fin cs.length} {v : (cs.get i).VPos} {w : (cs.get j).VPos} (h : childV i v = childV j w) : i = j

theorem Anderson4D.PlaneTree.childV_inj_snd {cs : List PlaneTree} {i : Fin cs.length} {v w : (cs.get i).VPos} (h : childV i v = childV i w) : v = w

theorem Anderson4D.PlaneTree.vpos_node_cases {cs : List PlaneTree} (P : (node cs).VPos → Prop) (hroot : P (node cs).rootV) (hchild : ∀ (i : Fin cs.length) (v : (cs.get i).VPos), P (childV i v)) (v : (node cs).VPos) : P v

theorem Anderson4D.PlaneTree.ne_root_iff {t : PlaneTree} {v : t.VPos} : v ≠ t.rootV ↔ ↑v ≠ []

@[simp]

theorem Anderson4D.PlaneTree.parentV_rootV {t : PlaneTree} : parentV t.rootV = t.rootV

@[simp]

theorem Anderson4D.PlaneTree.parentV_childV_rootV {cs : List PlaneTree} (i : Fin cs.length) : parentV (childV i (cs.get i).rootV) = (node cs).rootV

theorem Anderson4D.PlaneTree.parentV_childV {cs : List PlaneTree} (i : Fin cs.length) {v : (cs.get i).VPos} (hv : v ≠ (cs.get i).rootV) : parentV (childV i v) = childV i (parentV v)

theorem Anderson4D.PlaneTree.eq_rootV_of_parentV_eq {t : PlaneTree} {v : t.VPos} (h : parentV v = v) : v = t.rootV

theorem Anderson4D.PlaneTree.parentV_eq_root_cases {cs : List PlaneTree} {v : (node cs).VPos} (h : parentV v = (node cs).rootV) : v = (node cs).rootV ∨ ∃ (i : Fin cs.length), v = childV i (cs.get i).rootV

theorem Anderson4D.PlaneTree.exists_childV_of_parentV_eq {ds : List PlaneTree} {x : (node ds).VPos} {j : Fin ds.length} {u : (ds.get j).VPos} (h : parentV x = childV j u) : ∃ (u' : (ds.get j).VPos), x = childV j u'

Isomorphisms of unordered rooted trees

def Anderson4D.PlaneTree.Iso (s t : PlaneTree) : Type

An isomorphism between the unordered rooted trees presented by s and t: a parent-commuting bijection of vertices (for s = t this is exactly the defining property of autSubgroup).

Equations

• s.Iso t = { e : s.VPos ≃ t.VPos // ∀ (v : s.VPos), e (Anderson4D.PlaneTree.parentV v) = Anderson4D.PlaneTree.parentV (e v) }

instance Anderson4D.PlaneTree.instFiniteIso (s t : PlaneTree) : Finite (s.Iso t)

theorem Anderson4D.PlaneTree.Iso.ext {s t : PlaneTree} {e f : s.Iso t} (h : ∀ (v : s.VPos), ↑e v = ↑f v) : e = f

def Anderson4D.PlaneTree.Iso.refl (t : PlaneTree) : t.Iso t

The identity isomorphism.

Equations

• Anderson4D.PlaneTree.Iso.refl t = ⟨Equiv.refl t.VPos, ⋯⟩

def Anderson4D.PlaneTree.Iso.trans {s t u : PlaneTree} (e : s.Iso t) (f : t.Iso u) : s.Iso u

Composition of isomorphisms.

Equations

• e.trans f = ⟨(↑e).trans ↑f, ⋯⟩

def Anderson4D.PlaneTree.Iso.symm {s t : PlaneTree} (e : s.Iso t) : t.Iso s

Inverse of an isomorphism.

Equations

• e.symm = ⟨(↑e).symm, ⋯⟩

def Anderson4D.PlaneTree.Iso.ofEq {s t : PlaneTree} (h : s = t) : s.Iso t

Transport along an equality of trees.

Equations

• Anderson4D.PlaneTree.Iso.ofEq h = h ▸ Anderson4D.PlaneTree.Iso.refl s

def Anderson4D.PlaneTree.Iso.congr {s t s' t' : PlaneTree} (hs : s = s') (ht : t = t') (e : s.Iso t) : s'.Iso t'

Transport an isomorphism along equalities of its endpoints.

Equations

• Anderson4D.PlaneTree.Iso.congr hs ht e = (Anderson4D.PlaneTree.Iso.ofEq ⋯).trans (e.trans (Anderson4D.PlaneTree.Iso.ofEq ht))

@[simp]

theorem Anderson4D.PlaneTree.Iso.refl_apply {t : PlaneTree} (v : t.VPos) : ↑(refl t) v = v

@[simp]

theorem Anderson4D.PlaneTree.Iso.trans_apply {s t u : PlaneTree} (e : s.Iso t) (f : t.Iso u) (v : s.VPos) : ↑(e.trans f) v = ↑f (↑e v)

@[simp]

theorem Anderson4D.PlaneTree.Iso.symm_apply_apply {s t : PlaneTree} (e : s.Iso t) (v : s.VPos) : ↑e.symm (↑e v) = v

@[simp]

theorem Anderson4D.PlaneTree.Iso.apply_symm_apply {s t : PlaneTree} (e : s.Iso t) (v : t.VPos) : ↑e (↑e.symm v) = v

@[simp]

theorem Anderson4D.PlaneTree.Iso.symm_symm {s t : PlaneTree} (e : s.Iso t) : e.symm.symm = e

theorem Anderson4D.PlaneTree.Iso.root_eq {s t : PlaneTree} (e : s.Iso t) : ↑e s.rootV = t.rootV

Isomorphisms send the root to the root.

theorem Anderson4D.PlaneTree.Iso.apply_ne_root {s t : PlaneTree} (e : s.Iso t) {v : s.VPos} (hv : v ≠ s.rootV) : ↑e v ≠ t.rootV

def Anderson4D.PlaneTree.isoAutEquiv (t : PlaneTree) : t.Iso t ≃ t.Aut

Automorphisms are exactly the self-isomorphisms.

Equations

• t.isoAutEquiv = Equiv.subtypeEquivRight ⋯

Splitting a node's vertex set into root and child parts; grafting

def Anderson4D.PlaneTree.vposNodeEquiv (cs : List PlaneTree) : (node cs).VPos ≃ Option ((i : Fin cs.length) × (cs.get i).VPos)

The vertices of node cs are the root plus the vertices of the children.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Anderson4D.PlaneTree.vposNodeEquiv_root (cs : List PlaneTree) : (vposNodeEquiv cs) (node cs).rootV = none

@[simp]

theorem Anderson4D.PlaneTree.vposNodeEquiv_childV {cs : List PlaneTree} (i : Fin cs.length) (v : (cs.get i).VPos) : (vposNodeEquiv cs) (childV i v) = some ⟨i, v⟩

@[simp]

theorem Anderson4D.PlaneTree.vposNodeEquiv_symm_none (cs : List PlaneTree) : (vposNodeEquiv cs).symm none = (node cs).rootV

@[simp]

theorem Anderson4D.PlaneTree.vposNodeEquiv_symm_some {cs : List PlaneTree} (i : Fin cs.length) (v : (cs.get i).VPos) : (vposNodeEquiv cs).symm (some ⟨i, v⟩) = childV i v

def Anderson4D.PlaneTree.graftCarrier {cs ds : List PlaneTree} (π : Fin cs.length ≃ Fin ds.length) (F : (i : Fin cs.length) → (cs.get i).Iso (ds.get (π i))) : (node cs).VPos ≃ (node ds).VPos

Carrier bijection of a graft: permute children by π, act inside child i by F i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Anderson4D.PlaneTree.graftCarrier_root {cs ds : List PlaneTree} (π : Fin cs.length ≃ Fin ds.length) (F : (i : Fin cs.length) → (cs.get i).Iso (ds.get (π i))) : (graftCarrier π F) (node cs).rootV = (node ds).rootV

@[simp]

theorem Anderson4D.PlaneTree.graftCarrier_childV {cs ds : List PlaneTree} (π : Fin cs.length ≃ Fin ds.length) (F : (i : Fin cs.length) → (cs.get i).Iso (ds.get (π i))) (i : Fin cs.length) (v : (cs.get i).VPos) : (graftCarrier π F) (childV i v) = childV (π i) (↑(F i) v)

def Anderson4D.PlaneTree.graft {cs ds : List PlaneTree} (π : Fin cs.length ≃ Fin ds.length) (F : (i : Fin cs.length) → (cs.get i).Iso (ds.get (π i))) : (node cs).Iso (node ds)

Graft a permutation of the children together with per-child isomorphisms into an isomorphism of the nodes.

Equations

• Anderson4D.PlaneTree.graft π F = ⟨Anderson4D.PlaneTree.graftCarrier π F, ⋯⟩

@[simp]

theorem Anderson4D.PlaneTree.graft_apply_root {cs ds : List PlaneTree} (π : Fin cs.length ≃ Fin ds.length) (F : (i : Fin cs.length) → (cs.get i).Iso (ds.get (π i))) : ↑(graft π F) (node cs).rootV = (node ds).rootV

@[simp]

theorem Anderson4D.PlaneTree.graft_apply_childV {cs ds : List PlaneTree} (π : Fin cs.length ≃ Fin ds.length) (F : (i : Fin cs.length) → (cs.get i).Iso (ds.get (π i))) (i : Fin cs.length) (v : (cs.get i).VPos) : ↑(graft π F) (childV i v) = childV (π i) (↑(F i) v)

Splitting an isomorphism of nodes into child data

theorem Anderson4D.PlaneTree.vpos_node_cases_or {cs : List PlaneTree} (v : (node cs).VPos) : v = (node cs).rootV ∨ ∃ (i : Fin cs.length) (w : (cs.get i).VPos), v = childV i w

theorem Anderson4D.PlaneTree.exists_childIdx {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) : ∃ (j : Fin ds.length), ↑e (childV i (cs.get i).rootV) = childV j (ds.get j).rootV

An isomorphism of nodes maps depth-one vertices to depth-one vertices.

noncomputable def Anderson4D.PlaneTree.childIdx {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) : Fin ds.length

Index of the child onto which e maps child i.

Equations

• Anderson4D.PlaneTree.childIdx e i = ⋯.choose

theorem Anderson4D.PlaneTree.childIdx_spec {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) : ↑e (childV i (cs.get i).rootV) = childV (childIdx e i) (ds.get (childIdx e i)).rootV

theorem Anderson4D.PlaneTree.exists_childV_image {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) (v : (cs.get i).VPos) : ∃ (w : (ds.get (childIdx e i)).VPos), ↑e (childV i v) = childV (childIdx e i) w

e maps the whole subtree below child i into the subtree below child childIdx e i.

noncomputable def Anderson4D.PlaneTree.childMap {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) (v : (cs.get i).VPos) : (ds.get (childIdx e i)).VPos

The action of e inside child i, expressed in child childIdx e i.

Equations

• Anderson4D.PlaneTree.childMap e i v = ⋯.choose

theorem Anderson4D.PlaneTree.childMap_spec {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) (v : (cs.get i).VPos) : ↑e (childV i v) = childV (childIdx e i) (childMap e i v)

theorem Anderson4D.PlaneTree.childMap_root {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) : childMap e i (cs.get i).rootV = (ds.get (childIdx e i)).rootV

theorem Anderson4D.PlaneTree.childIdx_symm_childIdx {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) : childIdx e.symm (childIdx e i) = i

noncomputable def Anderson4D.PlaneTree.childEquiv {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) : Fin cs.length ≃ Fin ds.length

The permutation of children induced by an isomorphism of nodes.

Equations

• Anderson4D.PlaneTree.childEquiv e = { toFun := Anderson4D.PlaneTree.childIdx e, invFun := Anderson4D.PlaneTree.childIdx e.symm, left_inv := ⋯, right_inv := ⋯ }

theorem Anderson4D.PlaneTree.exists_childMap_preimage {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) (w : (ds.get (childIdx e i)).VPos) : ∃ (v : (cs.get i).VPos), ↑e (childV i v) = childV (childIdx e i) w

noncomputable def Anderson4D.PlaneTree.childIso {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) : (cs.get i).Iso (ds.get ((childEquiv e) i))

The isomorphism induced by e from child i onto child childEquiv e i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Anderson4D.PlaneTree.childIso_apply {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) (v : (cs.get i).VPos) : ↑(childIso e i) v = childMap e i v

@[simp]

theorem Anderson4D.PlaneTree.childEquiv_apply {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) (i : Fin cs.length) : (childEquiv e) i = childIdx e i

theorem Anderson4D.PlaneTree.graft_childEquiv_childIso {cs ds : List PlaneTree} (e : (node cs).Iso (node ds)) : graft (childEquiv e) (childIso e) = e

Splitting is a section of grafting.

theorem Anderson4D.PlaneTree.graft_injective {cs ds : List PlaneTree} : Function.Injective fun (x : (π : Fin cs.length ≃ Fin ds.length) × ((i : Fin cs.length) → (cs.get i).Iso (ds.get (π i)))) => graft x.fst x.snd

theorem Anderson4D.PlaneTree.graft_surjective {cs ds : List PlaneTree} : Function.Surjective fun (x : (π : Fin cs.length ≃ Fin ds.length) × ((i : Fin cs.length) → (cs.get i).Iso (ds.get (π i)))) => graft x.fst x.snd

theorem Anderson4D.PlaneTree.nat_card_iso_node {cs ds : List PlaneTree} : Nat.card ((node cs).Iso (node ds)) = ∑ π : Fin cs.length ≃ Fin ds.length, ∏ i : Fin cs.length, Nat.card ((cs.get i).Iso (ds.get (π i)))

Master counting step: isomorphisms of nodes are counted by a child permutation together with per-child isomorphisms.

theorem Anderson4D.PlaneTree.nat_card_iso_of_nonempty {s t : PlaneTree} (h : Nonempty (s.Iso t)) : Nat.card (s.Iso t) = Nat.card (s.Iso s)

Torsor step: a single isomorphism s ≅ t makes the isomorphisms a torsor under the self-isomorphisms of s.

Permutations of the children list give isomorphisms

def Anderson4D.PlaneTree.finExtend {n m : ℕ} (σ : Fin n ≃ Fin m) : Fin (n + 1) ≃ Fin (m + 1)

Extend an index bijection by fixing a new head index 0.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.PlaneTree.iso_of_perm {l l' : List PlaneTree} : l.Perm l' → Nonempty ((node l).Iso (node l'))

A permutation of a list of trees induces an isomorphism of the nodes.

Counting values of a list function via index fibers

theorem Anderson4D.PlaneTree.count_ofFn {β : Type} [BEq β] [LawfulBEq β] [DecidableEq β] {n : ℕ} (g : Fin n → β) (b : β) : List.count b (List.ofFn g) = {i : Fin n | g i = b}.card

theorem Anderson4D.PlaneTree.map_eq_ofFn {α β : Type} (l : List α) (f : α → β) : List.map f l = List.ofFn fun (i : Fin l.length) => f (l.get i)

theorem Anderson4D.PlaneTree.count_map_get {α β : Type} [BEq β] [LawfulBEq β] [DecidableEq β] (l : List α) (f : α → β) (b : β) : List.count b (List.map f l) = {i : Fin l.length | f (l.get i) = b}.card

theorem Anderson4D.PlaneTree.canonList_length (cs : List PlaneTree) : (canonList cs).length = cs.length

canonList entries.

theorem Anderson4D.PlaneTree.canonList_getElem (cs : List PlaneTree) (i : ℕ) (h : i < (canonList cs).length) (h' : i < cs.length) : (canonList cs)[i] = cs[i].canon

theorem Anderson4D.PlaneTree.nonempty_iso_canon (t : PlaneTree) : Nonempty (t.Iso t.canon)

Canonicalization does not change the unordered tree.

theorem Anderson4D.PlaneTree.canon_eq_of_iso (s t : PlaneTree) : ∀ (a : s.Iso t), s.canon = t.canon

Isomorphic trees have equal canonical forms.

Permutations preserving a classification

theorem Anderson4D.PlaneTree.fiberPerm_congr {ι κ : Type} (f : ι → κ) (u : (k : κ) → Equiv.Perm { i : ι // f i = k }) {k k' : κ} (h : k = k') (x : ι) (hx : f x = k) (hx' : f x = k') : ↑((u k) ⟨x, hx⟩) = ↑((u k') ⟨x, hx'⟩)

def Anderson4D.PlaneTree.assemblePerm {ι κ : Type} (f : ι → κ) (u : (k : κ) → Equiv.Perm { i : ι // f i = k }) : Equiv.Perm ι

Assemble a family of fiber permutations into a permutation of the base.

Equations

• Anderson4D.PlaneTree.assemblePerm f u = { toFun := fun (i : ι) => ↑((u (f i)) ⟨i, ⋯⟩), invFun := fun (i : ι) => ↑((Equiv.symm (u (f i))) ⟨i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }

def Anderson4D.PlaneTree.fiberPermEquiv {ι κ : Type} (f : ι → κ) : { π : Equiv.Perm ι // ∀ (i : ι), f (π i) = f i } ≃ ((k : κ) → Equiv.Perm { i : ι // f i = k })

Permutations preserving the classification f are families of permutations of the fibers of f.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.PlaneTree.nat_card_fiber_perms {ι κ : Type} [Fintype ι] [DecidableEq ι] [DecidableEq κ] (f : ι → κ) [Fintype κ] : Nat.card { π : Equiv.Perm ι // ∀ (i : ι), f (π i) = f i } = ∏ k : κ, (Nat.card { i : ι // f i = k }).factorial

theorem Anderson4D.PlaneTree.nat_card_pres_perms {ι : Type} [Fintype ι] [DecidableEq ι] {κ' : Type} [DecidableEq κ'] (g : ι → κ') : Nat.card { π : Equiv.Perm ι // ∀ (i : ι), g (π i) = g i } = ∏ k ∈ Finset.image g Finset.univ, (Nat.card { i : ι // g i = k }).factorial

Runs of key-equal elements in a sorted list

theorem Anderson4D.PlaneTree.go_pairwise (ds : List PlaneTree) (c : PlaneTree) (k : ℕ) : List.Pairwise KeyLe (c :: ds) → runsProdFactorial.go c k ds = (k + List.count c.key (List.map key ds)).factorial * ∏ j ∈ (List.map key ds).toFinset.erase c.key, (List.count j (List.map key ds)).factorial

theorem Anderson4D.PlaneTree.runsProdFactorial_pairwise {l : List PlaneTree} (h : List.Pairwise KeyLe l) : runsProdFactorial l = ∏ j ∈ (List.map key l).toFinset, (List.count j (List.map key l)).factorial

runsProdFactorial of a KeyLe-pairwise list is the product of the factorials of the key multiplicities.

Assembly helpers

theorem Anderson4D.PlaneTree.prod_ite_zero {n : ℕ} (p : Fin n → Prop) [DecidablePred p] (a : Fin n → ℕ) : (∏ i : Fin n, if p i then a i else 0) = if ∀ (i : Fin n), p i then ∏ i : Fin n, a i else 0

theorem Anderson4D.PlaneTree.nat_card_subtype_filter {α : Type} [Fintype α] (P : α → Prop) [DecidablePred P] : Nat.card { x : α // P x } = (Finset.filter P Finset.univ).card

theorem Anderson4D.PlaneTree.sum_ite_eq_card_mul {α : Type} [Fintype α] (P : α → Prop) [DecidablePred P] (C : ℕ) : (∑ x : α, if P x then C else 0) = Nat.card { x : α // P x } * C

theorem Anderson4D.PlaneTree.prod_autCard_get (cs : List PlaneTree) : ∏ i : Fin cs.length, (cs.get i).autCard = autCardList cs

The product of the children's autCards over Fin-indices.

theorem Anderson4D.PlaneTree.pres_card_eq_runs (cs : List PlaneTree) : Nat.card { π : Fin cs.length ≃ Fin cs.length // ∀ (i : Fin cs.length), (cs.get (π i)).canon = (cs.get i).canon } = runsProdFactorial (List.insertionSort KeyLe (canonList cs))

The canon-class-preserving permutation count is the run-factorial product of the canonically sorted children.

The D-hepp cross-check: |Aut t| = t.autCard

theorem Anderson4D.PlaneTree.card_aut_eq_autCard (t : PlaneTree) : Fintype.card t.Aut = t.autCard

Blueprint obligation (D-hepp cross-check).

The order of the automorphism group realized as parent-commuting vertex permutations (Aut) equals the recursive product formula autCard (run factorials on canonically sorted children × the children's own counts). Proof: strong induction on t; an automorphism of node cs fixes the root, permutes the depth-1 vertices by some σ with canon cs[σ i] = canon cs[i] and restricts to subtree isomorphisms, giving an equivalence of Aut (node cs) with (canon-class-preserving σ) × (a family of subtree isomorphism sets, each of cardinality autCard cs[i]); the σ-factor has runsProdFactorial many elements by key-injectivity. Kernel-checked instances follow below.