Finite trees in canonical offspring coordinates

The existing PlaneTree uses zero-based child indices. The locally finite carrier uses positive indices to match the existing BGW-law construction. positiveAddress is the explicit conversion; zero is always an invalid index on the locally finite side. All finite-tree reasoning uses the public list API.

def BGW.PlaneTree.positiveAddress (u : List ℕ) : List ℕ

Convert a zero-based address to its positive-index counterpart.

Equations

• BGW.PlaneTree.positiveAddress u = List.map Nat.succ u

@[simp]

theorem BGW.PlaneTree.positiveAddress_nil : positiveAddress [] = []

@[simp]

theorem BGW.PlaneTree.positiveAddress_cons (i : ℕ) (u : List ℕ) : positiveAddress (i :: u) = (i + 1) :: positiveAddress u

def BGW.PlaneTree.offspringAt : PlaneTree → List ℕ → ℕ

Offspring count at a positive-index address; invalid addresses have count zero.

Equations

• x✝.offspringAt [] = x✝.rootDegree
• x✝.offspringAt (0 :: tail) = 0
• x✝.offspringAt (i.succ :: u) = (Option.map (fun (s : BGW.PlaneTree) => s.offspringAt u) x✝.children[i]?).getD 0

@[simp]

theorem BGW.PlaneTree.offspringAt_nil (t : PlaneTree) : t.offspringAt [] = t.rootDegree

@[simp]

theorem BGW.PlaneTree.offspringAt_zero_cons (t : PlaneTree) (u : List ℕ) : t.offspringAt (0 :: u) = 0

theorem BGW.PlaneTree.canonical_offspringAt (t : PlaneTree) : LocallyFinite.Canonical t.offspringAt

def BGW.PlaneTree.toLocallyFinite (t : PlaneTree) : LocallyFinite.Tree

View a finite plane tree as a canonical, possibly-infinite-tree value.

Equations

• t.toLocallyFinite = ⟨t.offspringAt, ⋯⟩

@[simp]

theorem BGW.PlaneTree.degree_toLocallyFinite (t : PlaneTree) : LocallyFinite.degree t.toLocallyFinite = t.rootDegree

@[simp]

theorem BGW.PlaneTree.toLocallyFinite_leaf : leaf.toLocallyFinite = LocallyFinite.leaf

theorem BGW.PlaneTree.offspringAt_positiveAddress (t : PlaneTree) (u : List ℕ) : t.offspringAt (positiveAddress u) = (Option.map rootDegree (t.fringe? u)).getD 0

The positive-index coordinates agree with the original fringe lookup.

theorem BGW.PlaneTree.child_toLocallyFinite {t s : PlaneTree} (i : ℕ) (h : t.children[i]? = some s) : LocallyFinite.child t.toLocallyFinite (i + 1) = s.toLocallyFinite

An existing zero-based child becomes child i + 1 in the new carrier.

theorem BGW.PlaneTree.present_toLocallyFinite (t : PlaneTree) (u : List ℕ) : LocallyFinite.Present t.toLocallyFinite (positiveAddress u) ↔ t.IsVertex u

Vertex membership is preserved, including the root and leaves.

theorem BGW.PlaneTree.toLocallyFinite_injective : Function.Injective toLocallyFinite

Distinct finite trees stay distinct in the canonical offspring representation.

theorem BGW.PlaneTree.exists_positiveAddress_of_present {T : LocallyFinite.Tree} {u : List ℕ} (hu : LocallyFinite.Present T u) : ∃ (v : List ℕ), positiveAddress v = u

Every present positive-index address has a zero-based preimage.

theorem BGW.PlaneTree.finiteVertices_toLocallyFinite (t : PlaneTree) : LocallyFinite.FiniteVertices t.toLocallyFinite

theorem BGW.LocallyFinite.FiniteVertices.exists_height_bound {T : Tree} (hT : FiniteVertices T) : ∃ (n : ℕ), ∀ (u : Address), Present T u → List.length u ≤ n

A finite tree has a uniform bound on the depth of its vertices. Adapted from Freezing1/PlaneFiniteExtinction.lean, without its model imports.

def BGW.LocallyFinite.truncate : ℕ → Tree → PlaneTree

Cut at a deterministic depth, keeping the root and the order of children.

Equations

• BGW.LocallyFinite.truncate 0 x✝ = BGW.PlaneTree.leaf
• BGW.LocallyFinite.truncate n.succ x✝ = BGW.PlaneTree.node (List.ofFn fun (i : Fin (BGW.LocallyFinite.degree x✝)) => BGW.LocallyFinite.truncate n (BGW.LocallyFinite.child x✝ (↑i + 1)))

theorem BGW.LocallyFinite.toLocallyFinite_truncate_of_height_bound (n : ℕ) (T : Tree) (hT : ∀ (u : Address), Present T u → List.length u ≤ n) : (truncate n T).toLocallyFinite = T

Once the truncation depth bounds all vertices, no information is lost.

theorem BGW.LocallyFinite.exists_toLocallyFinite_iff (T : Tree) : (∃ (t : PlaneTree), t.toLocallyFinite = T) ↔ FiniteVertices T

The finite plane trees are exactly the locally finite trees with finitely many vertices.

noncomputable def BGW.PlaneTree.equivFiniteVertices : PlaneTree ≃ { T : LocallyFinite.Tree // LocallyFinite.FiniteVertices T }

The existing finite-tree type is equivalent to the finite part of the canonical carrier.

Equations

• BGW.PlaneTree.equivFiniteVertices = Equiv.ofBijective (fun (t : BGW.PlaneTree) => ⟨t.toLocallyFinite, ⋯⟩) BGW.PlaneTree.equivFiniteVertices._proof_2

@[simp]

theorem BGW.PlaneTree.equivFiniteVertices_apply (t : PlaneTree) : ↑(equivFiniteVertices t) = t.toLocallyFinite