Parent-function encoding of a connected child-link graph

Paper §5.3, Step 5 chooses a link tree on the children of a branching vertex and exposes the children from a fixed root. This file makes that choice canonical enough for counting:

• the children form the vertices of an undirected simple graph;
• two distinct children are adjacent when IsLink holds;
• LinkedChildren gives connectedness of this graph;
• SimpleGraph.parentTowardRoot orients one shortest-path edge toward a fixed root;
• graph distance strictly decreases along the parent map, so sorting by distance exposes every parent before its child;
• the parent map is literally an element of the full finite function space used by fullParentWeight.

IsLink itself can hold on the diagonal, so adjacency explicitly includes a ≠ b.

@[reducible, inline]

abbrev Anderson4D.BranchChild {t : PlaneTree} (v : t.VPos) : Type

The finite type of children of a fixed tree vertex.

Equations

• Anderson4D.BranchChild v = ↥(Anderson4D.childrenOf v)

theorem Anderson4D.isLink_symm {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v c c' : t.VPos} (h : IsLink Nm z v c c') : IsLink Nm z v c' c

The link relation is symmetric.

theorem Anderson4D.isLink_comm {t : PlaneTree} (Nm : t.HeppMarking) (z : LeafEmbedding t) (v c c' : t.VPos) : IsLink Nm z v c c' ↔ IsLink Nm z v c' c

def Anderson4D.childLinkGraph {t : PlaneTree} (Nm : t.HeppMarking) (z : LeafEmbedding t) (v : t.VPos) : SimpleGraph (BranchChild v)

Undirected simple graph of links among the children of v.

Equations

• Anderson4D.childLinkGraph Nm z v = { Adj := fun (a b : Anderson4D.BranchChild v) => a ≠ b ∧ Anderson4D.IsLink Nm z v ↑a ↑b, symm := ⋯, loopless := ⋯ }

@[simp]

theorem Anderson4D.childLinkGraph_adj {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} {a b : BranchChild v} : (childLinkGraph Nm z v).Adj a b ↔ a ≠ b ∧ IsLink Nm z v ↑a ↑b

theorem Anderson4D.branchChild_nonempty {t : PlaneTree} {v : t.VPos} (hv : v ∈ t.BranchNodes) : Nonempty (BranchChild v)

A branch vertex has at least one child, packaged as nonemptiness of the child subtype.

theorem Anderson4D.childLinkGraph_connected {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) : (childLinkGraph Nm z v).Connected

LinkedChildren is precisely enough to make the undirected child-link graph connected. Self-steps in its reflexive-transitive chain are discarded when converting to walks of the irreflexive graph.

Shortest-path parent map

noncomputable def Anderson4D.linkParent {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) : BranchChild v → BranchChild v

Orient a chosen shortest-path edge from every child toward the fixed root child. The root points to itself.

Equations

• Anderson4D.linkParent hv hlinked root = Anderson4D.SimpleGraph.parentTowardRoot (Anderson4D.childLinkGraph Nm z v) ⋯ root

@[simp]

theorem Anderson4D.linkParent_root {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) : linkParent hv hlinked root root = root

theorem Anderson4D.childLinkGraph_adj_linkParent {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) {c : BranchChild v} (hc : c ≠ root) : (childLinkGraph Nm z v).Adj c (linkParent hv hlinked root c)

Every non-root child is adjacent to its chosen parent.

theorem Anderson4D.isLink_linkParent {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) {c : BranchChild v} (hc : c ≠ root) : IsLink Nm z v ↑c ↑(linkParent hv hlinked root c)

In particular, the selected parent is linked to its child in the original geometric relation.

theorem Anderson4D.linkParent_ne_self {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) {c : BranchChild v} (hc : c ≠ root) : linkParent hv hlinked root c ≠ c

A non-root child never points to itself.

theorem Anderson4D.linkParent_dist_lt {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) {c : BranchChild v} (hc : c ≠ root) : (childLinkGraph Nm z v).dist (linkParent hv hlinked root c) root < (childLinkGraph Nm z v).dist c root

Following a selected parent strictly lowers graph distance to the fixed root.

Enumeration in increasing graph distance

noncomputable def Anderson4D.childrenByLinkDistance {t : PlaneTree} (Nm : t.HeppMarking) (z : LeafEmbedding t) (v : t.VPos) (root : BranchChild v) : List (BranchChild v)

All children, stably sorted by nondecreasing link-graph distance to the fixed root. Ties are harmless: the parent distance is strictly smaller.

Equations

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

@[simp]

theorem Anderson4D.mem_childrenByLinkDistance {t : PlaneTree} (Nm : t.HeppMarking) (z : LeafEmbedding t) (v : t.VPos) (root c : BranchChild v) : c ∈ childrenByLinkDistance Nm z v root

theorem Anderson4D.childrenByLinkDistance_nodup {t : PlaneTree} (Nm : t.HeppMarking) (z : LeafEmbedding t) (v : t.VPos) (root : BranchChild v) : (childrenByLinkDistance Nm z v root).Nodup

theorem Anderson4D.childrenByLinkDistance_pairwise {t : PlaneTree} (Nm : t.HeppMarking) (z : LeafEmbedding t) (v : t.VPos) (root : BranchChild v) : List.Pairwise (fun (a b : BranchChild v) => (childLinkGraph Nm z v).dist a root ≤ (childLinkGraph Nm z v).dist b root) (childrenByLinkDistance Nm z v root)

The distance enumeration is pairwise nondecreasing.

theorem Anderson4D.idxOf_linkParent_lt {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) {c : BranchChild v} (hc : c ≠ root) : List.idxOf (linkParent hv hlinked root c) (childrenByLinkDistance Nm z v root) < List.idxOf c (childrenByLinkDistance Nm z v root)

In the distance-sorted enumeration, every non-root child's parent occurs strictly earlier.

Interface to the full parent-function space

noncomputable def Anderson4D.linkParentFullFunction {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) : BranchChild v → BranchChild v

The selected link parent is already a full parent function, with no quotient or partial-domain conversion.

Equations

• Anderson4D.linkParentFullFunction hv hlinked root = Anderson4D.linkParent hv hlinked root

@[simp]

theorem Anderson4D.linkParentFullFunction_mem_univ {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) : linkParentFullFunction hv hlinked root ∈ Finset.univ

theorem Anderson4D.card_branchChild_fullFunctionSpace {t : PlaneTree} (v : t.VPos) : Fintype.card (BranchChild v → BranchChild v) = (childrenOf v).card ^ (childrenOf v).card

Size of the enlarged, directly countable full-function space.

theorem Anderson4D.fullParentWeight_linkParent {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) {R : Type u_1} [CommSemiring R] (parentWeight childWeight : BranchChild v → R) : fullParentWeight root parentWeight childWeight (linkParentFullFunction hv hlinked root) = ∏ c : BranchChild v, if c = root then 1 else parentWeight (linkParent hv hlinked root c) * childWeight c

fullParentWeight of the selected map has exactly the expected root-normalized edge-factor product.

theorem Anderson4D.fullParentWeight_linkParent_le_all_nat {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hlinked : LinkedChildren Nm z v) (root : BranchChild v) (parentWeight childWeight : BranchChild v → ℕ) : fullParentWeight root parentWeight childWeight (linkParentFullFunction hv hlinked root) ≤ ∏ c : BranchChild v, if c = root then 1 else (∑ u : BranchChild v, parentWeight u) * childWeight c

Natural weights of the selected parent map are bounded by the factorized sum over the full function space. This is the direct handoff to sum_fullParentWeight.