Parents, children and arms in a finite tree

Proof of Proposition 4.1, Step 2 (periodic-mesh-calculations.tex): "The tree is consequently a path or has one trivalent vertex. In the latter case let p ≤ q ≤ r be its arm lengths."

Seen from a root o, each other vertex has a unique parent (TreeBFS); its other neighbours are its children. This file sets up parents, children and ancestors.

noncomputable def MultiplicativeBasisDeformations.RootedTree.parentOf {D : Type v} [DecidableEq D] (G : SimpleGraph D) (hG : G.Connected) (o v : D) : D

The parent of a vertex, seen from the root o.

theorem MultiplicativeBasisDeformations.RootedTree.parentOf_spec {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {v : D} (h : v ≠ o) : G.Adj (parentOf G hG o v) v ∧ G.dist o (parentOf G hG o v) + 1 = G.dist o v

def MultiplicativeBasisDeformations.RootedTree.IsChild {D : Type v} (G : SimpleGraph D) (o v w : D) : Prop

w is a child of v.

theorem MultiplicativeBasisDeformations.RootedTree.eq_parentOf_of_isChild {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) {v w : D} (h : IsChild G o v w) : v = parentOf G hG o w

theorem MultiplicativeBasisDeformations.RootedTree.isChild_parentOf {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {w : D} (hw : w ≠ o) : IsChild G o (parentOf G hG o w) w

noncomputable def MultiplicativeBasisDeformations.RootedTree.children {D : Type v} [Fintype D] (G : SimpleGraph D) [DecidableRel G.Adj] (o v : D) : Finset D

The children of v.

theorem MultiplicativeBasisDeformations.RootedTree.degree_eq_one_add {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (par : D → ZMod 2) (hpar : ∀ {u w : D}, G.Adj u w → par w = par u + 1) (hG : G.Connected) (hA : G.IsAcyclic) (o : D) {v : D} (hv : v ≠ o) : G.degree v = 1 + (children G o v).card

A vertex other than the root has its parent and its children as neighbours.

theorem MultiplicativeBasisDeformations.RootedTree.degree_root {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (par : D → ZMod 2) (hpar : ∀ {u w : D}, G.Adj u w → par w = par u + 1) (hG : G.Connected) (o : D) : G.degree o = (children G o o).card

noncomputable def MultiplicativeBasisDeformations.RootedTree.anc {D : Type v} [DecidableEq D] (G : SimpleGraph D) (hG : G.Connected) (o : D) (k : ℕ) (v : D) : D

The k-th ancestor.

theorem MultiplicativeBasisDeformations.RootedTree.anc_succ {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) (k : ℕ) (v : D) : anc G hG o (k + 1) v = parentOf G hG o (anc G hG o k v)

theorem MultiplicativeBasisDeformations.RootedTree.dist_anc {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o v : D) (k : ℕ) : k ≤ G.dist o v → G.dist o (anc G hG o k v) = G.dist o v - k

theorem MultiplicativeBasisDeformations.RootedTree.anc_dist {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o v : D) : anc G hG o (G.dist o v) v = o

theorem MultiplicativeBasisDeformations.RootedTree.trivalent_unique {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (par : D → ZMod 2) (hpar : ∀ {u w : D}, G.Adj u w → par w = par u + 1) (hG : G.Connected) (hA : G.IsAcyclic) {n : D → ℚ} (hn : ∀ (i : D), 0 < n i) (hMn : ∀ (i : D), 0 < 2 * n i - ∑ j ∈ G.neighborFinset i, n j) {u w : D} (hu : G.degree u = 3) (hw : G.degree w = 3) : u = w

At most one trivalent vertex (periodic-mesh-calculations.tex).

noncomputable def MultiplicativeBasisDeformations.RootedTree.top {D : Type v} [DecidableEq D] (G : SimpleGraph D) (hG : G.Connected) (o v : D) : D

The child of the root through which the path to v passes.

theorem MultiplicativeBasisDeformations.RootedTree.dist_pos {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {v : D} (hv : v ≠ o) : 0 < G.dist o v

theorem MultiplicativeBasisDeformations.RootedTree.dist_top {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {v : D} (hv : v ≠ o) : G.dist o (top G hG o v) = 1

theorem MultiplicativeBasisDeformations.RootedTree.top_ne {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {v : D} (hv : v ≠ o) : top G hG o v ≠ o

theorem MultiplicativeBasisDeformations.RootedTree.parentOf_top {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {v : D} (hv : v ≠ o) : parentOf G hG o (top G hG o v) = o

theorem MultiplicativeBasisDeformations.RootedTree.top_mem_children {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {v : D} (hv : v ≠ o) : top G hG o v ∈ children G o o

theorem MultiplicativeBasisDeformations.RootedTree.top_of_dist_one {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {v : D} (hv : G.dist o v = 1) : top G hG o v = v

theorem MultiplicativeBasisDeformations.RootedTree.parentOf_ne {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {v : D} (hv : 2 ≤ G.dist o v) : parentOf G hG o v ≠ o

theorem MultiplicativeBasisDeformations.RootedTree.top_parentOf {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {v : D} (hv : 2 ≤ G.dist o v) : top G hG o (parentOf G hG o v) = top G hG o v

theorem MultiplicativeBasisDeformations.RootedTree.eq_of_top_eq_of_dist_eq {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) (d : ℕ) (v v' : D) : v ≠ o → v' ≠ o → G.dist o v = d + 1 → G.dist o v' = d + 1 → top G hG o v = top G hG o v' → v = v'

Each arm is a chain: below each child of the root there is at most one vertex at each distance, when non-root vertices have at most one child.

noncomputable def MultiplicativeBasisDeformations.RootedTree.arm {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) (hG : G.Connected) (o c : D) : Finset D

The arm below the child c of the root.

theorem MultiplicativeBasisDeformations.RootedTree.mem_arm {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {c v : D} : v ∈ arm G hG o c ↔ v ≠ o ∧ top G hG o v = c

theorem MultiplicativeBasisDeformations.RootedTree.self_mem_arm {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {c : D} (hc : c ∈ children G o o) : c ∈ arm G hG o c

theorem MultiplicativeBasisDeformations.RootedTree.image_dist_arm {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) {c : D} (hc : c ∈ children G o o) : Finset.image (G.dist o) (arm G hG o c) = Finset.Icc 1 (arm G hG o c).card

The distances along an arm are 1, …, |arm|.

noncomputable def MultiplicativeBasisDeformations.RootedTree.armVert {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) (hG : G.Connected) (o c : D) (d : ℕ) : D

The vertex of the arm below c at distance d.

theorem MultiplicativeBasisDeformations.RootedTree.armVert_spec {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) {c : D} (hc : c ∈ children G o o) {d : ℕ} (hd1 : 1 ≤ d) (hd2 : d ≤ (arm G hG o c).card) : armVert G hG o c d ∈ arm G hG o c ∧ G.dist o (armVert G hG o c d) = d

theorem MultiplicativeBasisDeformations.RootedTree.armVert_dist {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) {c v : D} (hc : c ∈ children G o o) (hv : v ∈ arm G hG o c) : armVert G hG o c (G.dist o v) = v

noncomputable def MultiplicativeBasisDeformations.RootedTree.enum {D : Type v} [Fintype D] (G : SimpleGraph D) [DecidableRel G.Adj] (o : D) : Fin (children G o o).card ≃ ↥(children G o o)

An enumeration of the children of the root.

noncomputable def MultiplicativeBasisDeformations.RootedTree.armLen {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) (i : Fin (children G o o).card) : ℕ

The arm lengths, minus one.

theorem MultiplicativeBasisDeformations.RootedTree.card_arm_pos {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) {c : D} (hc : c ∈ children G o o) : 1 ≤ (arm G hG o c).card

theorem MultiplicativeBasisDeformations.RootedTree.armLen_add_one {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) (i : Fin (children G o o).card) : armLen G hG o i + 1 = (arm G hG o ↑((enum G o) i)).card

theorem MultiplicativeBasisDeformations.RootedTree.dist_le_card_arm {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) {v : D} (hv : v ≠ o) : G.dist o v ≤ (arm G hG o (top G hG o v)).card

noncomputable def MultiplicativeBasisDeformations.RootedTree.toStarV {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) (v : D) : StarV (armLen G hG o)

The isomorphism with the star model, on vertices.

noncomputable def MultiplicativeBasisDeformations.RootedTree.fromStarV {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (o : D) : StarV (armLen G hG o) → D

The inverse of toStarV.

theorem MultiplicativeBasisDeformations.RootedTree.fromStarV_toStarV {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) (v : D) : fromStarV G hG o (toStarV G hG hA o hch v) = v

theorem MultiplicativeBasisDeformations.RootedTree.toStarV_fromStarV {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) (x : StarV (armLen G hG o)) : toStarV G hG hA o hch (fromStarV G hG o x) = x

theorem MultiplicativeBasisDeformations.RootedTree.adj_toStarV_aux {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (par : D → ZMod 2) (hpar : ∀ {u w : D}, G.Adj u w → par w = par u + 1) (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) {u v : D} (h : G.Adj u v) (hd : G.dist o v = G.dist o u + 1) : starAdj (toStarV G hG hA o hch u) (toStarV G hG hA o hch v)

theorem MultiplicativeBasisDeformations.RootedTree.adj_toStarV {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (par : D → ZMod 2) (hpar : ∀ {u w : D}, G.Adj u w → par w = par u + 1) (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) {u v : D} (h : G.Adj u v) : starAdj (toStarV G hG hA o hch u) (toStarV G hG hA o hch v)

theorem MultiplicativeBasisDeformations.RootedTree.armVert_one {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) {c : D} (hc : c ∈ children G o o) : armVert G hG o c 1 = c

theorem MultiplicativeBasisDeformations.RootedTree.adj_armVert_succ {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) {c : D} (hc : c ∈ children G o o) (k : ℕ) (hk : k + 2 ≤ (arm G hG o c).card) : G.Adj (armVert G hG o c (k + 1)) (armVert G hG o c (k + 2))

theorem MultiplicativeBasisDeformations.RootedTree.adj_fromStarV {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) {x y : StarV (armLen G hG o)} (h : starAdj x y) : G.Adj (fromStarV G hG o x) (fromStarV G hG o y)

noncomputable def MultiplicativeBasisDeformations.RootedTree.starEquiv {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) : D ≃ StarV (armLen G hG o)

The isomorphism with the star model, as an equivalence.

theorem MultiplicativeBasisDeformations.RootedTree.adj_iff_starAdj {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (par : D → ZMod 2) (hpar : ∀ {u w : D}, G.Adj u w → par w = par u + 1) (hG : G.Connected) (hA : G.IsAcyclic) (o : D) (hch : ∀ (v : D), v ≠ o → (children G o v).card ≤ 1) (u v : D) : G.Adj u v ↔ starAdj ((starEquiv G hG hA o hch) u) ((starEquiv G hG hA o hch) v)

theorem MultiplicativeBasisDeformations.RootedTree.classify_tree {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (par : D → ZMod 2) (hpar : ∀ {u w : D}, G.Adj u w → par w = par u + 1) (hG : G.Connected) (hA : G.IsAcyclic) [Nonempty D] {n : D → ℚ} (hn : ∀ (i : D), 0 < n i) (hMn : ∀ (i : D), 0 < 2 * n i - ∑ j ∈ G.neighborFinset i, n j) : ∃ (t : ℕ) (L : Fin t → ℕ) (e : D ≃ StarV L), (∀ (u v : D), G.Adj u v ↔ starAdj (e u) (e v)) ∧ (t ≤ 1 ∨ t = 3 ∧ ∑ i : Fin t, (↑(L i) + 1) / (↑(L i) + 2) < 2)

Proposition 4.1, Step 2: the tree is Dynkin. A finite tree carrying a vector n > 0 with Mn > 0 is a star with at most one arm (a path rooted at an end) or with three arms satisfying ∑ p_i/(p_i + 1) < 2 (periodic-mesh-calculations.tex).