Quantitative counting for the Hepp-tree carrier

Paper: L-5.2 — tree counting via the Dyck-word injection

This is paper Lemma 5.2 for Anderson4D.PlaneTree, the carrier used by the formalization.

A valid tree with at most r leaves is injected into Fin (4 * r + 1) × (Fin (4 * r) → Bool) through the balanced-parentheses key. This gives the explicit bound 4 ^ (4 * r). The final declarations package the sets of trees with at most, and exactly, r leaves as actual Finset PlaneTrees.

Size and key bounds on the real carrier

theorem Anderson4D.PlaneTree.size_add_one_le_of_isValid (t : PlaneTree) : t.isValid = true → t.size + 1 ≤ 2 * t.leafCount

A real-carrier valid Hepp tree has at most twice as many vertices as leaves, in subtraction-free form.

theorem Anderson4D.PlaneTree.size_le_of_isValid (t : PlaneTree) (ht : t.isValid = true) : t.size ≤ 2 * t.leafCount - 1

Paper Lemma 5.2, size part, on Anderson4D.PlaneTree.

theorem Anderson4D.PlaneTree.key_length (t : PlaneTree) : t.key.length = 2 * t.size

Each vertex of a real-carrier tree contributes one opening and one closing symbol to its key.

theorem Anderson4D.PlaneTree.key_mem (t : PlaneTree) (x : ℕ) : x ∈ t.key → x = 0 ∨ x = 1

Every symbol in a real-carrier tree key is either 0 or 1.

Explicit encoding and cardinality

@[reducible, inline]

abbrev Anderson4D.PlaneTree.ValidTreesAtMost (r : ℕ) : Type

The type of valid real-carrier trees having at most r leaves.

Equations

• Anderson4D.PlaneTree.ValidTreesAtMost r = { t : Anderson4D.PlaneTree // t.isValid = true ∧ t.leafCount ≤ r }

def Anderson4D.PlaneTree.validTreeCode (r : ℕ) : ValidTreesAtMost r → Fin (4 * r + 1) × (Fin (4 * r) → Bool)

Bounded binary-word code used to count ValidTreesAtMost r.

Equations

• Anderson4D.PlaneTree.validTreeCode r t = (⟨(↑t).key.length, ⋯⟩, fun (i : Fin (4 * r)) => (↑t).key.getD (↑i) 0 == 1)

theorem Anderson4D.PlaneTree.validTreeCode_injective (r : ℕ) : Function.Injective (validTreeCode r)

The bounded binary-word code is injective.

instance Anderson4D.PlaneTree.validTreesAtMostFinite (r : ℕ) : Finite (ValidTreesAtMost r)

@[implicit_reducible]

noncomputable instance Anderson4D.PlaneTree.validTreesAtMostFintype (r : ℕ) : Fintype (ValidTreesAtMost r)

Equations

• Anderson4D.PlaneTree.validTreesAtMostFintype r = Fintype.ofFinite (Anderson4D.PlaneTree.ValidTreesAtMost r)

theorem Anderson4D.PlaneTree.card_validTreesAtMost_type_le (r : ℕ) : Fintype.card (ValidTreesAtMost r) ≤ 4 ^ (4 * r)

Quantitative real-carrier version of paper Lemma 5.2.

noncomputable def Anderson4D.PlaneTree.validTreesAtMost (r : ℕ) : Finset PlaneTree

The actual finite set of valid real-carrier trees with at most r leaves.

Equations

• Anderson4D.PlaneTree.validTreesAtMost r = Finset.image (fun (t : Anderson4D.PlaneTree.ValidTreesAtMost r) => ↑t) Finset.univ

@[simp]

theorem Anderson4D.PlaneTree.mem_validTreesAtMost {r : ℕ} {t : PlaneTree} : t ∈ validTreesAtMost r ↔ t.isValid = true ∧ t.leafCount ≤ r

theorem Anderson4D.PlaneTree.card_validTreesAtMost_le (r : ℕ) : (validTreesAtMost r).card ≤ 4 ^ (4 * r)

Cardinality bound for the concrete Finset of valid trees with at most r leaves.

theorem Anderson4D.PlaneTree.finite_validTreesAtMost (r : ℕ) : {t : PlaneTree | t.isValid = true ∧ t.leafCount ≤ r}.Finite

The corresponding finite-set statement, for clients formulated with Set.Finite or Nat.card.

noncomputable def Anderson4D.PlaneTree.validTreesExactly (r : ℕ) : Finset PlaneTree

The actual finite set of valid real-carrier trees with exactly r leaves.

Equations

• Anderson4D.PlaneTree.validTreesExactly r = {t ∈ Anderson4D.PlaneTree.validTreesAtMost r | t.leafCount = r}

@[simp]

theorem Anderson4D.PlaneTree.mem_validTreesExactly {r : ℕ} {t : PlaneTree} : t ∈ validTreesExactly r ↔ t.isValid = true ∧ t.leafCount = r

theorem Anderson4D.PlaneTree.card_validTreesExactly_le (r : ℕ) : (validTreesExactly r).card ≤ 4 ^ (4 * r)

Cardinality bound for valid real-carrier trees with exactly r leaves.