WindowSpanSum.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.WindowSpanSum.preorderLengths line 12

Source documentation

The window lengths in edge preorder; the first length is that of the incoming edge, followed by its complete descendant block.

def preorderLengths (M g r₀ : ℕ) : ℕ → List ℕ
  | 0 => []
  | h + 1 => (List.replicate M
      (WindowRecursion.length M g r₀ (h + 1) :: preorderLengths M g r₀ h)).flatten

/-- Charge a gap after every entry, including the final entry. -/

Mentions: OAI.Problem310.WindowRecursion.length

def OAI.Problem310.WindowSpanSum.paddedSum line 18
Source documentation
Charge a gap after every entry, including the final entry.
```
def paddedSum (g : ℕ) (L : List ℕ) : ℕ := (L.map (fun r => r + g)).sum
```
theorem OAI.Problem310.WindowSpanSum.paddedSum_nil line 20
theorem OAI.Problem310.WindowSpanSum.paddedSum_cons line 22
theorem OAI.Problem310.WindowSpanSum.paddedSum_append line 25
theorem OAI.Problem310.WindowSpanSum.paddedSum_flatten_replicate line 29
theorem OAI.Problem310.WindowSpanSum.last_gap line 37
theorem OAI.Problem310.WindowSpanSum.paddedSum_preorderLengths line 41
Source documentation
The exact recursive span is the preorder padded sum with the final gap removed.
```
theorem paddedSum_preorderLengths (M g r₀ h : ℕ) (hM : 1 ≤ M) :
    paddedSum g (preorderLengths M g r₀ h) =
      if h = 0 then 0 else span M g r₀ h + g := by
…
```
Mentions: OAI.Problem310.WindowSpanSum.paddedSum, OAI.Problem310.WindowSpanSum.preorderLengths
theorem OAI.Problem310.WindowSpanSum.paddedSum_childBlock line 61
Source documentation
A child block has its precise geometric span plus one terminal gap.
```
theorem paddedSum_childBlock (M g r₀ h : ℕ) (hM : 1 ≤ M) :
    paddedSum g (WindowRecursion.length M g r₀ (h + 1) :: preorderLengths M g r₀ h) =
      childSpan M g r₀ h + g := by
…
```
Mentions: OAI.Problem310.WindowSpanSum.paddedSum, OAI.Problem310.WindowRecursion.length, OAI.Problem310.WindowSpanSum.preorderLengths
theorem OAI.Problem310.WindowSpanSum.childBlock_budget line 70
Source documentation
This is exactly the padded-length budget consumed by WindowPlacement.block_padding.
```
theorem childBlock_budget (M g r₀ h : ℕ) (hM : 1 ≤ M) :
    paddedSum g (WindowRecursion.length M g r₀ (h + 1) :: preorderLengths M g r₀ h) ≤
      2 * WindowRecursion.length M g r₀ (h + 1) + g := by
…
```
Mentions: OAI.Problem310.WindowSpanSum.paddedSum, OAI.Problem310.WindowRecursion.length, OAI.Problem310.WindowSpanSum.preorderLengths
theorem OAI.Problem310.WindowSpanSum.block_padding_of_child_sum line 78
Source documentation
Any consecutive rank slice having the child-block padded sum inherits padding. The caller only needs to identify its rank slice with the child's preorder block.
```
theorem block_padding_of_child_sum {len : ℕ → ℕ} {g i m M r₀ h : ℕ}
    (hM : 1 ≤ M) (hlen : 0 < len (i + m))
    (hsum : (∑ k ∈ Finset.range (m + 1), (len (i + k) + g)) =
      paddedSum g (WindowRecursion.length M g r₀ (h + 1) :: preorderLengths M g r₀ h)) :
    WindowPlacement.finish len g (i + m) - WindowPlacement.start len g i + 1 ≤
      2 * WindowRecursion.length M g r₀ (h + 1) := by
…
```
Mentions: OAI.Problem310.WindowSpanSum.paddedSum, OAI.Problem310.WindowRecursion.length, OAI.Problem310.WindowSpanSum.preorderLengths, OAI.Problem310.WindowPlacement.finish, OAI.Problem310.WindowPlacement.start
theorem OAI.Problem310.WindowSpanSum.block_endpoint_bound_of_child_sum line 90
Source documentation
The endpoint form needed by the concrete window metadata avoids natural subtraction and needs no positivity premise on an arbitrary rank sequence.
```
theorem block_endpoint_bound_of_child_sum {len : ℕ → ℕ} {g i m M r₀ h : ℕ}
    (hM : 1 ≤ M)
    (hsum : (∑ k ∈ Finset.range (m + 1), (len (i + k) + g)) =
      paddedSum g (WindowRecursion.length M g r₀ (h + 1) :: preorderLengths M g r₀ h)) :
    WindowPlacement.finish len g (i + m) + 1 ≤ WindowPlacement.start len g i +
      2 * WindowRecursion.length M g r₀ (h + 1) := by
…
```
Mentions: OAI.Problem310.WindowSpanSum.paddedSum, OAI.Problem310.WindowRecursion.length, OAI.Problem310.WindowSpanSum.preorderLengths, OAI.Problem310.WindowPlacement.finish, OAI.Problem310.WindowPlacement.start
theorem OAI.Problem310.WindowSpanSum.threshold_le_of_mem_preorderLengths line 102
Source documentation
Every serialized window retains the common threshold, including descendants.
```
theorem threshold_le_of_mem_preorderLengths (M g r₀ h : ℕ) :
    ∀ r ∈ preorderLengths M g r₀ h, r₀ ≤ r := by
…
```
Mentions: OAI.Problem310.WindowSpanSum.preorderLengths
theorem OAI.Problem310.WindowSpanSum.childBlock_ne_nil line 116
Source documentation
No child block is empty: its incoming window is always the first entry.
```
theorem childBlock_ne_nil (M g r₀ h : ℕ) :
    WindowRecursion.length M g r₀ (h + 1) :: preorderLengths M g r₀ h ≠ [] := by
…
```
Mentions: OAI.Problem310.WindowRecursion.length, OAI.Problem310.WindowSpanSum.preorderLengths
theorem OAI.Problem310.WindowSpanSum.positive_of_mem_childBlock line 121
Source documentation
Positivity needed to turn padded rank sums into inclusive endpoint bounds.
```
theorem positive_of_mem_childBlock {M g r₀ h r : ℕ} (hr₀ : 0 < r₀)
    (hr : r ∈ WindowRecursion.length M g r₀ (h + 1) :: preorderLengths M g r₀ h) :
    0 < r := by
…
```
Mentions: OAI.Problem310.WindowRecursion.length, OAI.Problem310.WindowSpanSum.preorderLengths