Parent maps extracted from finite connected graphs

The Hepp-tree volume argument repeatedly chooses a link tree on the children of a branch. For counting, it is enough to orient one shortest-path edge from every non-root vertex toward a fixed root. The resulting parent map strictly lowers graph distance, so the vertices can be exposed in increasing distance order. We keep the parent map inside the full function space α → α; summing over that larger space factorizes coordinatewise.

noncomputable def Anderson4D.SimpleGraph.shortestWalkToRoot {α : Type u_1} (G : SimpleGraph α) (hG : G.Connected) (root v : α) : G.Walk v root

A chosen shortest walk from v to root in a connected graph.

Equations

• Anderson4D.SimpleGraph.shortestWalkToRoot G hG root v = Classical.choose ⋯

@[simp]

theorem Anderson4D.SimpleGraph.shortestWalkToRoot_length {α : Type u_1} (G : SimpleGraph α) (hG : G.Connected) (root v : α) : (shortestWalkToRoot G hG root v).length = G.dist v root

noncomputable def Anderson4D.SimpleGraph.parentTowardRoot {α : Type u_1} (G : SimpleGraph α) [DecidableEq α] (hG : G.Connected) (root v : α) : α

The canonical parent of root is itself; every other vertex points to the second vertex of a chosen shortest walk to root.

Equations

• Anderson4D.SimpleGraph.parentTowardRoot G hG root v = if v = root then root else (Anderson4D.SimpleGraph.shortestWalkToRoot G hG root v).snd

@[simp]

theorem Anderson4D.SimpleGraph.parentTowardRoot_root {α : Type u_1} (G : SimpleGraph α) [DecidableEq α] (hG : G.Connected) (root : α) : parentTowardRoot G hG root root = root

theorem Anderson4D.SimpleGraph.adj_parentTowardRoot {α : Type u_1} (G : SimpleGraph α) [DecidableEq α] (hG : G.Connected) (root : α) {v : α} (hv : v ≠ root) : G.Adj v (parentTowardRoot G hG root v)

Every non-root parent edge is an edge of the original graph.

theorem Anderson4D.SimpleGraph.dist_parentTowardRoot_lt {α : Type u_1} (G : SimpleGraph α) [DecidableEq α] (hG : G.Connected) (root : α) {v : α} (hv : v ≠ root) : G.dist (parentTowardRoot G hG root v) root < G.dist v root

Following the chosen parent strictly decreases distance to the root.

theorem Anderson4D.SimpleGraph.parentTowardRoot_ne_self {α : Type u_1} (G : SimpleGraph α) [DecidableEq α] (hG : G.Connected) (root : α) {v : α} (hv : v ≠ root) : parentTowardRoot G hG root v ≠ v

In particular, a parent chain cannot cycle away from the root.

Coordinatewise sum over the enlarged parent-map space

def Anderson4D.fullParentWeight {α : Type u_1} {R : Type u_2} [Fintype α] [DecidableEq α] [CommSemiring R] (root : α) (parentWeight childWeight : α → R) (p : α → α) : R

Weight of a full parent map. The root coordinate contributes 1; at a non-root vertex v, the factor separates into the weight of its chosen parent and a vertex-local child weight.

Equations

• Anderson4D.fullParentWeight root parentWeight childWeight p = ∏ v : α, if v = root then if p v = root then 1 else 0 else parentWeight (p v) * childWeight v

theorem Anderson4D.sum_fullParentWeight {α : Type u_1} {R : Type u_2} [Fintype α] [DecidableEq α] [CommSemiring R] (root : α) (parentWeight childWeight : α → R) : ∑ p : α → α, fullParentWeight root parentWeight childWeight p = ∏ v : α, if v = root then 1 else (∑ u : α, parentWeight u) * childWeight v

Exact factorization of the sum over all full parent maps.

theorem Anderson4D.sum_fullParentWeight_subset_nat {α : Type u_1} [Fintype α] [DecidableEq α] [DecidableEq (α → α)] (root : α) (parentWeight childWeight : α → ℕ) (P : Finset (α → α)) : ∑ p ∈ P, fullParentWeight root parentWeight childWeight p ≤ ∏ v : α, if v = root then 1 else (∑ u : α, parentWeight u) * childWeight v

Natural-valued restriction to any finite family of parent maps.