Trees seen from a root

Elementary facts about a finite tree with a proper two-colouring, used in the proof of Proposition 4.1, Step 2 (periodic-mesh-calculations.tex): seen from a root o, adjacent vertices have distances differing by one, and every other vertex has a unique neighbour closer to o (its parent).

theorem MultiplicativeBasisDeformations.TreeBFS.walk_length_parity {D : Type v} {G : SimpleGraph D} (par : D → ZMod 2) (hpar : ∀ {u w : D}, G.Adj u w → par w = par u + 1) {u w : D} (p : G.Walk u w) : ↑p.length = par w - par u

theorem MultiplicativeBasisDeformations.TreeBFS.dist_adj {D : Type v} {G : SimpleGraph D} (par : D → ZMod 2) (hpar : ∀ {u w : D}, G.Adj u w → par w = par u + 1) (hG : G.Connected) (o : D) {u w : D} (h : G.Adj u w) : G.dist o w = G.dist o u + 1 ∨ G.dist o u = G.dist o w + 1

Adjacent vertices have distances to the root differing by exactly one.

theorem MultiplicativeBasisDeformations.TreeBFS.exists_parent {D : Type v} {G : SimpleGraph D} (hG : G.Connected) (o : D) {v : D} (hv : v ≠ o) : ∃ (u : D), G.Adj u v ∧ G.dist o u + 1 = G.dist o v

Every vertex other than the root has a neighbour closer to the root.

theorem MultiplicativeBasisDeformations.TreeBFS.parent_unique {D : Type v} {G : SimpleGraph D} (hG : G.Connected) (hA : G.IsAcyclic) (o : D) {v u u' : D} (h : G.Adj u v) (hu : G.dist o u + 1 = G.dist o v) (h' : G.Adj u' v) (hu' : G.dist o u' + 1 = G.dist o v) : u = u'

In a tree, the parent is unique.