TreeSpanBridge.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.TreeSpanBridge.weights line 13
Source documentation
Incoming-window lengths listed in the tree's edge preorder.
```
def weights (q d : ℕ) (r : ℕ → ℕ) : List ℕ :=
…
```
theorem OAI.Problem310.TreeSpanBridge.weights_zero line 16
theorem OAI.Problem310.TreeSpanBridge.weights_succ line 20
Source documentation
Each child contributes its incoming length followed by the weights of a complete subtree of one smaller height. This is independent of the child label.
```
theorem weights_succ (q d : ℕ) (r : ℕ → ℕ) :
    weights q (d + 1) r =
      (List.finRange q).flatMap (fun _ => r (d + 1) :: weights q d r) := by
…
```
Mentions: OAI.Problem310.TreeSpanBridge.weights
def OAI.Problem310.TreeSpanBridge.subtreeBlock line 35
Source documentation
An edge and all descendants under it, in their contiguous preorder block.
```
def subtreeBlock (q d : ℕ) (p : List (Fin q)) : List (List (Fin q)) :=
…
```
theorem OAI.Problem310.TreeSpanBridge.childBlock_infix line 38
theorem OAI.Problem310.TreeSpanBridge.subtreeBlock_infix line 45
Source documentation
Every rooted descendant block is contiguous in the global edge preorder.
```
theorem subtreeBlock_infix (q d : ℕ) (p : List (Fin q))
    (hp : p ≠ []) (hlen : p.length ≤ d) :
    subtreeBlock q d p <:+: edgePaths q d := by
…
```
Mentions: OAI.Problem310.TreeSpanBridge.subtreeBlock
theorem OAI.Problem310.TreeSpanBridge.map_weights_subtreeBlock line 68
Source documentation
Global-depth weights on one descendant block are exactly the incoming length followed by the weights of the complete residual-height subtree.
```
theorem map_weights_subtreeBlock (q d : ℕ) (r : ℕ → ℕ) (p : List (Fin q))
    (hlen : p.length ≤ d) :
    (subtreeBlock q d p).map (fun v => r (d + 1 - v.length)) =
      r (d + 1 - p.length) :: weights q (d - p.length) r := by
…
```
Mentions: OAI.Problem310.TreeSpanBridge.subtreeBlock, OAI.Problem310.TreeSpanBridge.weights
theorem OAI.Problem310.TreeSpanBridge.weights_subtree_infix line 82
Source documentation
The incoming edge and descendant weights form a contiguous block of the full weighted preorder, ready for the numerical child-span estimate.
```
theorem weights_subtree_infix (q d : ℕ) (r : ℕ → ℕ) (p : List (Fin q))
    (hp : p ≠ []) (hlen : p.length ≤ d) :
    (r (d + 1 - p.length) :: weights q (d - p.length) r) <:+: weights q d r := by
…
```
Mentions: OAI.Problem310.TreeSpanBridge.weights

theorem OAI.Problem310.TreeSpanBridge.take_drop_idxOf_of_infix line 90

Source documentation

A nonempty contiguous block in a duplicate-free list starts at the index of its first entry.

theorem take_drop_idxOf_of_infix {α : Type u_α} [BEq α] [LawfulBEq α]
    (l : List α) (hl : l.Nodup) (a : α) (u : List α) (h : (a :: u) <:+: l) :
    (l.drop (l.idxOf a)).take (u.length + 1) = a :: u := by
…

theorem OAI.Problem310.TreeSpanBridge.subtreeBlock_eq_slice line 102

Source documentation

Exact contiguous slice of the preorder belonging to one rooted child block.

theorem subtreeBlock_eq_slice (q d : ℕ) (p : List (Fin q))
    (hp : p ≠ []) (hlen : p.length ≤ d) :
    ((edgePaths q d).drop ((edgePaths q d).idxOf p)).take
      (1 + edgeCount q (d - p.length)) = subtreeBlock q d p := by
…

Mentions: OAI.Problem310.TreeSpanBridge.subtreeBlock

theorem OAI.Problem310.TreeSpanBridge.weights_slice line 113

Source documentation

The weighted preorder slice at an edge is its incoming weight followed by exactly one residual-height weighted subtree.

theorem weights_slice (q d : ℕ) (r : ℕ → ℕ) (p : List (Fin q))
    (hp : p ≠ []) (hlen : p.length ≤ d) :
    ((weights q d r).drop ((edgePaths q d).idxOf p)).take
      (1 + edgeCount q (d - p.length)) =
      r (d + 1 - p.length) :: weights q (d - p.length) r := by
…

Mentions: OAI.Problem310.TreeSpanBridge.weights

theorem OAI.Problem310.TreeSpanBridge.weights_eq_preorderLengths line 122
Source documentation
The path-dependent weight list is exactly the numerical preorder list.
```
theorem weights_eq_preorderLengths (q g r₀ d : ℕ) :
    weights q d (WindowRecursion.length q g r₀) =
      WindowSpanSum.preorderLengths q g r₀ d := by
…
```
Mentions: OAI.Problem310.TreeSpanBridge.weights, OAI.Problem310.WindowRecursion.length, OAI.Problem310.WindowSpanSum.preorderLengths

theorem OAI.Problem310.TreeSpanBridge.paddedSum_weights_slice line 132

Source documentation

The exact padded sum of the actual subtree slice in global preorder.

theorem paddedSum_weights_slice (q g r₀ d : ℕ) (hq : 1 ≤ q) (p : List (Fin q))
    (hp : p ≠ []) (hlen : p.length ≤ d) :
    WindowSpanSum.paddedSum g
      (((weights q d (WindowRecursion.length q g r₀)).drop
        ((edgePaths q d).idxOf p)).take (1 + edgeCount q (d - p.length))) =
      WindowRecursion.childSpan q g r₀ (d - p.length) + g := by
…

Mentions: OAI.Problem310.WindowSpanSum.paddedSum, OAI.Problem310.TreeSpanBridge.weights, OAI.Problem310.WindowRecursion.length, OAI.Problem310.WindowRecursion.childSpan

theorem OAI.Problem310.TreeSpanBridge.paddedSum_weights_slice_le line 145

Source documentation

The arithmetic padding budget now applies to an actual subtree slice, not merely to an abstract recursively defined list of lengths.

theorem paddedSum_weights_slice_le (q g r₀ d : ℕ) (hq : 1 ≤ q) (p : List (Fin q))
    (hp : p ≠ []) (hlen : p.length ≤ d) :
    WindowSpanSum.paddedSum g
      (((weights q d (WindowRecursion.length q g r₀)).drop
        ((edgePaths q d).idxOf p)).take (1 + edgeCount q (d - p.length))) ≤
      2 * WindowRecursion.length q g r₀ (d + 1 - p.length) + g := by
…

Mentions: OAI.Problem310.WindowSpanSum.paddedSum, OAI.Problem310.TreeSpanBridge.weights, OAI.Problem310.WindowRecursion.length

theorem OAI.Problem310.TreeSpanBridge.weighted_child_decomposition line 159

Source documentation

Full-list decomposition at the genuine edge index. This is the direct interface for constructing separated windows from the weighted preorder.

theorem weighted_child_decomposition (q g r₀ d : ℕ) (p : List (Fin q))
    (hp : p ≠ []) (hlen : p.length ≤ d) :
    ∃ pre post : List ℕ,
      weights q d (WindowRecursion.length q g r₀) =
        pre ++ (WindowRecursion.length q g r₀ (d + 1 - p.length) ::
          WindowSpanSum.preorderLengths q g r₀ (d - p.length)) ++ post ∧
      pre.length = (edgePaths q d).idxOf p := by
…

Mentions: OAI.Problem310.TreeSpanBridge.weights, OAI.Problem310.WindowRecursion.length, OAI.Problem310.WindowSpanSum.preorderLengths