Canonical locally finite plane trees

This is the deterministic carrier used by the iid offspring construction in freezing1/Freezing1/PlaneTree.lean and PlaneTreeGeometry.lean, adapted into BGW.LocallyFinite. Unlike BGW.PlaneTree, its trees may have infinite height.

Addresses use positive child indices, with [] for the root. Offspring counts are zero at absent addresses, but also at leaves: vertex membership is Present, not positivity of the coordinate. The finite-tree bridge explicitly shifts the existing zero-based addresses. No topology or probability law is installed here.

@[reducible, inline]

abbrev BGW.LocallyFinite.Address : Type

A vertex address, with positive child indices and [] for the root.

Equations

• BGW.LocallyFinite.Address = List ℕ

@[reducible, inline]

abbrev BGW.LocallyFinite.Offspring : Type

A field assigning a finite offspring count to each address.

Equations

• BGW.LocallyFinite.Offspring = (BGW.LocallyFinite.Address → ℕ)

def BGW.LocallyFinite.Canonical (f : Offspring) : Prop

Invalid children have zero offspring; the condition propagates to descendants.

Equations

• BGW.LocallyFinite.Canonical f = ∀ (u : BGW.LocallyFinite.Address) (j : ℕ), ¬(1 ≤ j ∧ j ≤ f u) → f (u ++ [j]) = 0

@[reducible, inline]

abbrev BGW.LocallyFinite.Tree : Type

Canonical offspring fields describe possibly infinite, locally finite plane trees.

Equations

• BGW.LocallyFinite.Tree = { f : BGW.LocallyFinite.Offspring // BGW.LocallyFinite.Canonical f }

def BGW.LocallyFinite.degree (T : Tree) : ℕ

The number of children of the root.

Equations

• BGW.LocallyFinite.degree T = ↑T []

def BGW.LocallyFinite.leaf : Tree

The tree consisting only of its root, with zero offspring at every address.

Equations

• BGW.LocallyFinite.leaf = ⟨fun (x : BGW.LocallyFinite.Address) => 0, BGW.LocallyFinite.leaf._proof_1⟩

@[simp]

theorem BGW.LocallyFinite.leaf_offspring (u : Address) : ↑leaf u = 0

@[simp]

theorem BGW.LocallyFinite.degree_leaf : degree leaf = 0

theorem BGW.LocallyFinite.Canonical.zero_descendants {f : Offspring} (hf : Canonical f) {u : Address} (hu : f u = 0) (v : Address) : f (u ++ v) = 0

theorem BGW.LocallyFinite.Canonical.zero_of_absent_child {f : Offspring} (hf : Canonical f) (u : Address) (j : ℕ) (hj : ¬(1 ≤ j ∧ j ≤ f u)) (v : Address) : f (u ++ j :: v) = 0

theorem BGW.LocallyFinite.eq_leaf_of_degree_zero {T : Tree} (hT : degree T = 0) : T = leaf

theorem BGW.LocallyFinite.degree_zero_iff (T : Tree) : degree T = 0 ↔ T = leaf

def BGW.LocallyFinite.child (T : Tree) (j : ℕ) : Tree

Re-root at child j. An absent child is represented by leaf; use Present to test whether that child actually exists.

Equations

• BGW.LocallyFinite.child T j = ⟨fun (u : BGW.LocallyFinite.Address) => ↑T (j :: u), ⋯⟩

@[simp]

theorem BGW.LocallyFinite.child_offspring (T : Tree) (j : ℕ) (u : Address) : ↑(child T j) u = ↑T (j :: u)

theorem BGW.LocallyFinite.child_eq_leaf_of_absent (T : Tree) (j : ℕ) (hj : ¬(1 ≤ j ∧ j ≤ degree T)) : child T j = leaf

theorem BGW.LocallyFinite.eq_of_degree_child_eq {T S : Tree} (hd : degree T = degree S) (hc : ∀ (j : ℕ), 1 ≤ j → j ≤ degree T → child T j = child S j) : T = S

The root degree and its existing ordered children determine a tree.

def BGW.LocallyFinite.Present (T : Tree) : Address → Prop

Membership of an address, including leaves and the root.

Equations

• BGW.LocallyFinite.Present T [] = True
• BGW.LocallyFinite.Present T (j :: u) = (1 ≤ j ∧ j ≤ BGW.LocallyFinite.degree T ∧ BGW.LocallyFinite.Present (BGW.LocallyFinite.child T j) u)

@[simp]

theorem BGW.LocallyFinite.present_nil (T : Tree) : Present T []

@[simp]

theorem BGW.LocallyFinite.present_cons (T : Tree) (j : ℕ) (u : Address) : Present T (j :: u) ↔ 1 ≤ j ∧ j ≤ degree T ∧ Present (child T j) u

theorem BGW.LocallyFinite.not_present_offspring_zero (T : Tree) (u : Address) (hu : ¬Present T u) : ↑T u = 0

def BGW.LocallyFinite.FiniteVertices (T : Tree) : Prop

Finiteness refers to the vertices, not to the support of the offspring field.

Equations

• BGW.LocallyFinite.FiniteVertices T = {u : BGW.LocallyFinite.Address | BGW.LocallyFinite.Present T u}.Finite