Admissible embeddings of marked Hepp trees (nodes D-adm, L-5.5)

Paper Def 5.4 and Lemma 5.5 of arXiv:2607.10105, in the simple case (multiplicities deferred).

• lcaPath, lcaV — least common ancestor of two vertices, via the longest common prefix of position paths.
• scaleN — the dyadic scale N_v = 2 ^ Nm.Nexp v of a vertex under a marking (junk off branch nodes, where Nexp is unconstrained).
• leavesUnder, childrenOf — the leaves of the subtree at a vertex, and the children of a vertex, as Finsets of position-prefix conditions.
• IsAdmissible — Def 5.4: injective, leaf-pair separation N_{l ∨ l'} / 2 ≤ |z l − z l'|, values bounded by M, and the children of every branch node connected by chains of links; the chain condition (Def 5.4(b)) is Relation.ReflTransGen of the one-link relation IsLink.
• Realizes — a marked tree realizes a finite set Z if some admissible embedding has image exactly Z.
• exists_star_realizes — Lemma 5.5 in the single-scale case (stage 2'): a nonempty bounded set whose pairwise distances lie in the dyadic window [2^N/2, 2^N] is realized by a star tree with constant marking N (or by the bare leaf when it is a singleton).

Longest common prefix and least common ancestors

def Anderson4D.lcaPath : List ℕ → List ℕ → List ℕ

Longest common prefix of two position paths: the position of the least common ancestor of the two vertices.

Equations

• Anderson4D.lcaPath [] x✝ = []
• Anderson4D.lcaPath (head :: tail) [] = []
• Anderson4D.lcaPath (a :: as) (b :: bs) = if a = b then a :: Anderson4D.lcaPath as bs else []

@[simp]

theorem Anderson4D.lcaPath_self (p : List ℕ) : lcaPath p p = p

theorem Anderson4D.lcaPath_comm (p q : List ℕ) : lcaPath p q = lcaPath q p

theorem Anderson4D.lcaPath_prefix_left (p q : List ℕ) : lcaPath p q <+: p

The longest common prefix is a prefix of the first argument.

theorem Anderson4D.lcaPath_prefix_right (p q : List ℕ) : lcaPath p q <+: q

The longest common prefix is a prefix of the second argument.

theorem Anderson4D.IsPos_of_prefix {t : PlaneTree} {p q : PlaneTree.Pos} (hp : t.IsPos p) (hq : q <+: p) : t.IsPos q

Position validity descends to prefixes: a prefix of a valid position is a valid position (it is an iterated dropLast).

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

The least common ancestor of two vertices (longest common prefix of their position paths).

Equations

• Anderson4D.lcaV v w = ⟨Anderson4D.lcaPath ↑v ↑w, ⋯⟩

theorem Anderson4D.lcaV_comm {t : PlaneTree} (v w : t.VPos) : lcaV v w = lcaV w v

@[simp]

theorem Anderson4D.lcaV_self {t : PlaneTree} (v : t.VPos) : lcaV v v = v

Scales, subtree leaves, children

def Anderson4D.scaleN {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : ℕ

The dyadic scale N_v = 2 ^ Nm.Nexp v of a vertex under a marking. Off the branch nodes Nm.Nexp is unconstrained junk, and so is scaleN; all statements below only inspect it at branch nodes (or under a constant marking).

Equations

• Anderson4D.scaleN Nm v = 2 ^ Nm.Nexp v

theorem Anderson4D.scaleN_pos {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : 0 < scaleN Nm v

def Anderson4D.leavesUnder {t : PlaneTree} (v : t.VPos) : Finset ↥t.Leaves

The leaves of the subtree rooted at v: leaves whose position extends v's.

Equations

• Anderson4D.leavesUnder v = {l : ↥t.Leaves | ↑v <+: ↑↑l}

@[simp]

theorem Anderson4D.mem_leavesUnder {t : PlaneTree} {v : t.VPos} {l : ↥t.Leaves} : l ∈ leavesUnder v ↔ ↑v <+: ↑↑l

theorem Anderson4D.self_mem_leavesUnder {t : PlaneTree} (v : t.VPos) (hv : v ∈ t.Leaves) : ⟨v, hv⟩ ∈ leavesUnder v

A leaf belongs to the leaves under itself.

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

The children of a vertex: valid positions extending v's by one step.

Equations

• Anderson4D.childrenOf v = {w : t.VPos | List.length ↑w = List.length ↑v + 1 ∧ ↑v <+: ↑w}

@[simp]

theorem Anderson4D.mem_childrenOf {t : PlaneTree} {v w : t.VPos} : w ∈ childrenOf v ↔ List.length ↑w = List.length ↑v + 1 ∧ ↑v <+: ↑w

Admissible embeddings (paper Def 5.4, simple case)

def Anderson4D.IsLink {t : PlaneTree} (Nm : t.HeppMarking) (z : ↥t.Leaves → Fin 4 → ℤ) (v c c' : t.VPos) : Prop

One link at scale N_v (Def 5.4(b)): the subtrees at c and c' contain leaves whose embedded points are at distance at most N_v.

Equations

• Anderson4D.IsLink Nm z v c c' = ∃ l ∈ Anderson4D.leavesUnder c, ∃ l' ∈ Anderson4D.leavesUnder c', Anderson4D.znorm (z l - z l') ≤ ↑(Anderson4D.scaleN Nm v)

def Anderson4D.LinkedChildren {t : PlaneTree} (Nm : t.HeppMarking) (z : ↥t.Leaves → Fin 4 → ℤ) (v : t.VPos) : Prop

Def 5.4(b): any two children of v are joined by a chain of links between children of v — the reflexive-transitive closure of the one-link relation, restricted to childrenOf v.

Equations

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

structure Anderson4D.IsAdmissible {t : PlaneTree} (Nm : t.HeppMarking) (M : ℕ) (z : ↥t.Leaves → Fin 4 → ℤ) : Prop

Paper Def 5.4 (simple case, multiplicities deferred): an admissible embedding of the leaves of a marked Hepp tree into ℤ⁴. (a): distinct leaves are separated by half the scale of their least common ancestor; (b): the children of every branch node are chained by links at its scale; all values lie in the box [-M, M]⁴.

• inj : Function.Injective z

  The embedding is injective.

• sep (l l' : ↥t.Leaves) : l ≠ l' → ↑(scaleN Nm (lcaV ↑l ↑l')) / 2 ≤ znorm (z l - z l')

  Def 5.4(a): separation by the scale of the least common ancestor.

• bounded (l : ↥t.Leaves) (i : Fin 4) : |z l i| ≤ ↑M

  All coordinates lie in [-M, M].

• linked (v : t.VPos) : v ∈ t.BranchNodes → LinkedChildren Nm z v

  Def 5.4(b): links connect the children of every branch node.

def Anderson4D.Realizes {t : PlaneTree} (Nm : t.HeppMarking) (M : ℕ) (Z : Finset (Fin 4 → ℤ)) : Prop

A marked Hepp tree realizes the finite set Z ⊆ ℤ⁴ (with box bound M) if some admissible embedding of its leaves has image exactly Z.

Equations

• Anderson4D.Realizes Nm M Z = ∃ (z : ↥t.Leaves → Fin 4 → ℤ), Anderson4D.IsAdmissible Nm M z ∧ Finset.image z Finset.univ = Z

Star trees (single-scale case of Lemma 5.5)

def Anderson4D.starTree (n : ℕ) : PlaneTree

The star tree: a root with n leaf children.

Equations

• Anderson4D.starTree n = Anderson4D.PlaneTree.node (List.replicate n Anderson4D.PlaneTree.leaf)

theorem Anderson4D.isPos_leaf_iff {p : PlaneTree.Pos} : PlaneTree.leaf.IsPos p ↔ p = []

The only valid position in the bare leaf is the root.

theorem Anderson4D.vpos_leaf_eq (v : PlaneTree.leaf.VPos) : v = PlaneTree.leaf.rootV

Every vertex of the bare leaf is the root.

theorem Anderson4D.isPos_starTree_iff {n : ℕ} {p : PlaneTree.Pos} : (starTree n).IsPos p ↔ p = [] ∨ ∃ i < n, p = [i]

The valid positions of the star tree: the root and the n leaves.

theorem Anderson4D.childCount_starTree_nil (n : ℕ) : (starTree n).childCount [] = n

The root of the star tree has n children.

theorem Anderson4D.childCount_starTree_leaf {n i : ℕ} : (starTree n).childCount [i] = 0

The depth-one vertices of the star tree are childless.

theorem Anderson4D.isValidList_replicate_leaf (m : ℕ) : PlaneTree.isValidList (List.replicate m PlaneTree.leaf) = true

Companion: a forest of leaves is Hepp-valid.

theorem Anderson4D.starTree_isValid {n : ℕ} (hn : n ≠ 1) : (starTree n).isValid = true

The star tree with n ≠ 1 children is Hepp-valid (no unary vertices).

theorem Anderson4D.leafCountList_replicate_leaf (m : ℕ) : PlaneTree.leafCountList (List.replicate m PlaneTree.leaf) = m

Companion: a forest of m leaves has m leaves.

theorem Anderson4D.leafCount_starTree {n : ℕ} (hn : 1 ≤ n) : (starTree n).leafCount = n

The star tree has n leaves (as counted by leafCount).

@[simp]

theorem Anderson4D.mem_Leaves_iff {t : PlaneTree} {v : t.VPos} : v ∈ t.Leaves ↔ t.childCount ↑v = 0

@[simp]

theorem Anderson4D.mem_BranchNodes_iff {t : PlaneTree} {v : t.VPos} : v ∈ t.BranchNodes ↔ 2 ≤ t.childCount ↑v

theorem Anderson4D.root_mem_leaves_leaf : PlaneTree.leaf.rootV ∈ PlaneTree.leaf.Leaves

theorem Anderson4D.branchNodes_leaf : PlaneTree.leaf.BranchNodes = ∅

The bare leaf has no branch nodes.

def Anderson4D.starLeafV (n : ℕ) (i : Fin n) : (starTree n).VPos

The i-th leaf vertex of the star tree.

Equations

• Anderson4D.starLeafV n i = ⟨[↑i], ⋯⟩

theorem Anderson4D.starLeafV_injective (n : ℕ) : Function.Injective (starLeafV n)

theorem Anderson4D.leaves_starTree {n : ℕ} (hn : 2 ≤ n) : (starTree n).Leaves = Finset.image (starLeafV n) Finset.univ

The leaves of the star tree are exactly its depth-one vertices.

theorem Anderson4D.card_leaves_starTree {n : ℕ} (hn : 2 ≤ n) : (starTree n).Leaves.card = n

theorem Anderson4D.branch_star_eq_root {n : ℕ} {v : (starTree n).VPos} (hv : v ∈ (starTree n).BranchNodes) : v = (starTree n).rootV

Every branch node of the star tree is the root.

theorem Anderson4D.mem_childrenOf_root_star {n : ℕ} {c : (starTree n).VPos} (hc : c ∈ childrenOf (starTree n).rootV) : ∃ i < n, ↑c = [i]

The children of the star-tree root are the depth-one positions.

theorem Anderson4D.starChild_mem_leaves {n : ℕ} {c : (starTree n).VPos} {i : ℕ} (hc : ↑c = [i]) : c ∈ (starTree n).Leaves

A depth-one vertex of the star tree is a leaf.

def Anderson4D.starMarking (n N : ℕ) (hN : 1 ≤ N) : (starTree n).HeppMarking

The constant marking N ≥ 1 on the star tree (its only branch node is the root, so parent_gt is vacuous).

Equations

• Anderson4D.starMarking n N hN = { Nexp := fun (x : (Anderson4D.starTree n).VPos) => N, pos := ⋯, parent_gt := ⋯ }

@[simp]

theorem Anderson4D.scaleN_starMarking {n N : ℕ} (hN : 1 ≤ N) (v : (starTree n).VPos) : ↑(scaleN (starMarking n N hN) v) = 2 ^ N

def Anderson4D.leafMarking (N : ℕ) : PlaneTree.leaf.HeppMarking

Any constant exponent is a Hepp marking of the bare leaf (no branch nodes, so both constraints are vacuous).

Equations

• Anderson4D.leafMarking N = { Nexp := fun (x : Anderson4D.PlaneTree.leaf.VPos) => N, pos := ⋯, parent_gt := ⋯ }

Realization (paper Lemma 5.5, single-scale case)

theorem Anderson4D.realizes_leaf (M N : ℕ) (x₀ : Fin 4 → ℤ) (hbound : ∀ (i : Fin 4), |x₀ i| ≤ ↑M) : Realizes (leafMarking N) M {x₀}

The bare leaf realizes any bounded singleton: all Def 5.4 conditions are vacuous for a single leaf.

theorem Anderson4D.realizes_star (M N : ℕ) (hN : 1 ≤ N) (Z : Finset (Fin 4 → ℤ)) (hn : 2 ≤ Z.card) (hbound : ∀ x ∈ Z, ∀ (i : Fin 4), |x i| ≤ ↑M) (hsep : ∀ x ∈ Z, ∀ y ∈ Z, x ≠ y → 2 ^ N / 2 ≤ znorm (x - y)) (hlink : ∀ x ∈ Z, ∀ y ∈ Z, znorm (x - y) ≤ 2 ^ N) : Realizes (starMarking Z.card N hN) M Z

The star tree on Z.card leaves with the constant marking N realizes any Z with at least two points, all pairwise distances in the dyadic window [2^N/2, 2^N], and coordinates bounded by M.

theorem Anderson4D.exists_star_realizes (M N : ℕ) (hN : 1 ≤ N) (Z : Finset (Fin 4 → ℤ)) (hZ : Z.Nonempty) (hbound : ∀ x ∈ Z, ∀ (i : Fin 4), |x i| ≤ ↑M) (hsep : ∀ x ∈ Z, ∀ y ∈ Z, x ≠ y → 2 ^ N / 2 ≤ znorm (x - y)) (hlink : ∀ x ∈ Z, ∀ y ∈ Z, znorm (x - y) ≤ 2 ^ N) : ∃ (t : PlaneTree) (_ : t.isValid = true) (Nm : t.HeppMarking), Realizes Nm M Z ∧ t.leafCount = Z.card ∧ ∀ v ∈ t.BranchNodes, Nm.Nexp v = N

Lemma 5.5, single-scale case (stage 2'): a nonempty set Z ⊆ [-M, M]⁴ whose pairwise distances all lie in one dyadic window [2^N/2, 2^N] is realized by a valid marked Hepp tree with Z.card leaves — the bare leaf if Z is a singleton, else the star tree with constant marking N (so every branch node carries exactly the exponent N).

Sanity checks (kernel-evaluated)