Branching.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Counting active leaves in a full ordered tree

A node is its path, a list of child labels. activeLeafCount A v h counts the active descendants exactly h edges below v. The condition BranchesAtLeast A k v h concerns only internal nodes of that finite subtree; it makes no assertion about children below its leaves.

def OAI.TreeEdit.BinaryLower.Branching.activeChildCount line 18
def OAI.TreeEdit.BinaryLower.Branching.activeLeafCount line 23
def OAI.TreeEdit.BinaryLower.Branching.BranchesAtLeast line 29
theorem OAI.TreeEdit.BinaryLower.Branching.pow_le_activeLeafCount line 37
Source documentation
If every active internal node has at least k active children, then an active root has at least k ^ h active leaves at depth h. No branching condition is imposed below depth h.
```
theorem pow_le_activeLeafCount (A : List α → Prop) (k h : ℕ)
    (v : List α) (hbranch : BranchesAtLeast A k v h) (hv : A v) :
    k ^ h ≤ activeLeafCount A v h := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Branching.BranchesAtLeast, OAI.TreeEdit.BinaryLower.Branching.activeLeafCount
theorem OAI.TreeEdit.BinaryLower.Branching.branchesAtLeast_of_local line 62
Source documentation
A level-bounded local branching assumption supplies exactly the finite recursive condition, with no assertion below the terminal level.
```
theorem branchesAtLeast_of_local (A : List α → Prop) (k H h : ℕ)
    (hlocal : ∀ v : List α, v.length < H → A v → k ≤ activeChildCount A v)
    (v : List α) (hv : v.length + h ≤ H) : BranchesAtLeast A k v h := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Branching.activeChildCount, OAI.TreeEdit.BinaryLower.Branching.BranchesAtLeast
theorem OAI.TreeEdit.BinaryLower.Branching.activeLeafCount_eq_card line 77
Source documentation
The recursive count is the ordinary finite cardinality of active paths of length h, represented by functions on Fin h.
```
theorem activeLeafCount_eq_card (A : List α → Prop) [DecidablePred A] (v : List α) (h : ℕ) :
    activeLeafCount A v h =
      (Finset.univ.filter fun f : Fin h → α => A (v ++ List.ofFn f)).card := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Branching.activeLeafCount

theorem OAI.TreeEdit.BinaryLower.Branching.pow_le_card_active_paths line 105

Source documentation

Explicit cardinality form of the active branching bound.

theorem pow_le_card_active_paths (A : List α → Prop) [DecidablePred A] (k h : ℕ)
    (v : List α) (hbranch : BranchesAtLeast A k v h) (hv : A v) :
    k ^ h ≤
      (Finset.univ.filter fun f : Fin h → α => A (v ++ List.ofFn f)).card := by
…

Mentions: OAI.TreeEdit.BinaryLower.Branching.BranchesAtLeast