TreePreorderRank.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.TreePreorderRank.size line 8

Source documentation

Number of nodes, including the root, in the complete K-ary tree of depth d.

def size (K : ℕ) : ℕ → ℕ
  | 0 => 1
  | d + 1 => 1 + K * size K d

/-- Preorder rank of a path. On paths of length at most `d`, this is the usual
zero-based root-first rank in the complete tree. -/

Mentions: OAI.Problem310.TreePreorderRank.rank

def OAI.Problem310.TreePreorderRank.rank line 14
Source documentation
Preorder rank of a path. On paths of length at most d, this is the usual zero-based root-first rank in the complete tree.
```
def rank {K : ℕ} : ℕ → List (Fin K) → ℕ
  | 0, _ => 0
  | _ + 1, [] => 0
  | d + 1, i :: p => 1 + i.val * size K d + rank d p
```
Mentions: OAI.Problem310.TreePreorderRank.size
theorem OAI.Problem310.TreePreorderRank.size_zero line 19
theorem OAI.Problem310.TreePreorderRank.size_succ line 20
theorem OAI.Problem310.TreePreorderRank.rank_nil line 21
theorem OAI.Problem310.TreePreorderRank.rank_cons line 23
theorem OAI.Problem310.TreePreorderRank.size_pos line 26
theorem OAI.Problem310.TreePreorderRank.rank_lt_size line 30
Source documentation
Every valid node has rank strictly below the total number of nodes.
```
theorem rank_lt_size {K d : ℕ} {p : List (Fin K)} (hp : p.length ≤ d) :
    rank d p < size K d := by
…
```
Mentions: OAI.Problem310.TreePreorderRank.rank, OAI.Problem310.TreePreorderRank.size
theorem OAI.Problem310.TreePreorderRank.rank_pos line 46
Source documentation
A nonroot valid node has positive rank.
```
theorem rank_pos {K d : ℕ} {p : List (Fin K)}
    (hp : p.length ≤ d) (hne : p ≠ []) : 0 < rank d p := by
…
```
Mentions: OAI.Problem310.TreePreorderRank.rank
theorem OAI.Problem310.TreePreorderRank.rank_append line 56
Source documentation
Descending into a node adds the local preorder rank in that node's subtree.
```
theorem rank_append {K d : ℕ} {p : List (Fin K)} (hp : p.length ≤ d)
    (q : List (Fin K)) :
    rank d (p ++ q) = rank d p + rank (d - p.length) q := by
…
```
Mentions: OAI.Problem310.TreePreorderRank.rank
theorem OAI.Problem310.TreePreorderRank.rank_append_bounds line 71
Source documentation
A subtree occupies one contiguous interval of the preorder ranks.
```
theorem rank_append_bounds {K d : ℕ} {p q : List (Fin K)}
    (hpq : (p ++ q).length ≤ d) :
    rank d p ≤ rank d (p ++ q) ∧
      rank d (p ++ q) < rank d p + size K (d - p.length) := by
…
```
Mentions: OAI.Problem310.TreePreorderRank.rank, OAI.Problem310.TreePreorderRank.size
theorem OAI.Problem310.TreePreorderRank.rank_lt_rank_append line 81
Source documentation
Every strict descendant occurs after its ancestor in preorder.
```
theorem rank_lt_rank_append {K d : ℕ} {p q : List (Fin K)}
    (hpq : (p ++ q).length ≤ d) (hq : q ≠ []) : rank d p < rank d (p ++ q) := by
…
```
Mentions: OAI.Problem310.TreePreorderRank.rank
theorem OAI.Problem310.TreePreorderRank.rank_cons_lt_rank_cons line 89
Source documentation
The entire subtree of an earlier child precedes the entire subtree of a later child.
```
theorem rank_cons_lt_rank_cons {K d : ℕ} {i j : Fin K} {p q : List (Fin K)}
    (hij : i < j) (hp : p.length ≤ d) (_hq : q.length ≤ d) :
    rank (d + 1) (i :: p) < rank (d + 1) (j :: q) := by
…
```
Mentions: OAI.Problem310.TreePreorderRank.rank

theorem OAI.Problem310.TreePreorderRank.rank_sibling_descendants_lt line 99

Source documentation

Ordered sibling subtrees remain ordered after any common ancestral prefix.

theorem rank_sibling_descendants_lt {K d : ℕ} {P p q : List (Fin K)} {i j : Fin K}
    (hij : i < j) (hp : (P ++ i :: p).length ≤ d)
    (hq : (P ++ j :: q).length ≤ d) :
    rank d (P ++ i :: p) < rank d (P ++ j :: q) := by
…

Mentions: OAI.Problem310.TreePreorderRank.rank

theorem OAI.Problem310.TreePreorderRank.rank_injective_on line 113
Source documentation
Preorder ranks distinguish every two valid paths.
```
theorem rank_injective_on {K d : ℕ} {p q : List (Fin K)}
    (hp : p.length ≤ d) (hq : q.length ≤ d) (heq : rank d p = rank d q) : p = q := by
…
```
Mentions: OAI.Problem310.TreePreorderRank.rank
theorem OAI.Problem310.TreePreorderRank.subtree_end_le_size line 142
Source documentation
The interval occupied by a subtree is contained in the whole tree's interval.
```
theorem subtree_end_le_size {K d : ℕ} {p : List (Fin K)} (hp : p.length ≤ d) :
    rank d p + size K (d - p.length) ≤ size K d := by
…
```
Mentions: OAI.Problem310.TreePreorderRank.rank, OAI.Problem310.TreePreorderRank.size
theorem OAI.Problem310.TreePreorderRank.isPrefix_iff_rank_bounds line 158
Source documentation
The descendants of a path are exactly a contiguous half-open interval of ranks.
```
theorem isPrefix_iff_rank_bounds {K d : ℕ} {p q : List (Fin K)}
    (hp : p.length ≤ d) (hq : q.length ≤ d) :
    List.IsPrefix p q ↔ rank d p ≤ rank d q ∧
      rank d q < rank d p + size K (d - p.length) := by
…
```
Mentions: OAI.Problem310.TreePreorderRank.rank, OAI.Problem310.TreePreorderRank.size
def OAI.Problem310.TreePreorderRank.edgeRank line 203
Source documentation
Zero-based rank among edges, obtained by removing the root's rank.
```
def edgeRank {K : ℕ} (d : ℕ) (p : List (Fin K)) : ℕ := rank d p - 1
```
Mentions: OAI.Problem310.TreePreorderRank.rank
theorem OAI.Problem310.TreePreorderRank.edgeRank_add_one line 205
theorem OAI.Problem310.TreePreorderRank.edgeRank_lt line 211
theorem OAI.Problem310.TreePreorderRank.edgeRank_injective_on line 218
theorem OAI.Problem310.TreePreorderRank.edgeRank_lt_edgeRank_append line 224
theorem OAI.Problem310.TreePreorderRank.edgeRank_sibling_descendants_lt line 233

theorem OAI.Problem310.TreePreorderRank.isPrefix_iff_edgeRank_bounds line 243

Source documentation

Edge ranks give the same exact contiguous-subtree characterization without the root slot.

theorem isPrefix_iff_edgeRank_bounds {K d : ℕ} {p q : List (Fin K)}
    (hp : p.length ≤ d) (hq : q.length ≤ d) (hp0 : p ≠ []) (hq0 : q ≠ []) :
    List.IsPrefix p q ↔ edgeRank d p ≤ edgeRank d q ∧
      edgeRank d q < edgeRank d p + size K (d - p.length) := by
…

Mentions: OAI.Problem310.TreePreorderRank.edgeRank, OAI.Problem310.TreePreorderRank.size