ListRunPrefix.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Prefix preservation in an append-only list sequence

Each step appends a finite list to the preceding state. The accumulated length is a finite sum, and all earlier entries retain their original indices.

theorem OAI.ReflexiveFixedPoints.ListRunPrefix.length_eq_sum line 20

Source documentation

Starting from the empty list, the length is the sum of all appended lengths.

theorem length_eq_sum (state extra : ℕ → List R)
    (hzero : state 0 = [])
    (hstep : ∀ n, state (n + 1) = state n ++ extra n) (n : ℕ) :
    (state n).length = ∑ i ∈ Finset.range n, (extra i).length := by
…

theorem OAI.ReflexiveFixedPoints.ListRunPrefix.prefix_of_le line 30

Source documentation

Every earlier state is an actual initial segment of every later state.

theorem prefix_of_le (state extra : ℕ → List R)
    (hstep : ∀ n, state (n + 1) = state n ++ extra n)
    {i j : ℕ} (h : i ≤ j) :
    state i <+: state j := by
…

theorem OAI.ReflexiveFixedPoints.ListRunPrefix.length_le_of_le line 41

Source documentation

Lengths cannot decrease along the append sequence.

theorem length_le_of_le (state extra : ℕ → List R)
    (hstep : ∀ n, state (n + 1) = state n ++ extra n)
    {i j : ℕ} (h : i ≤ j) :
    (state i).length ≤ (state j).length :=
…

theorem OAI.ReflexiveFixedPoints.ListRunPrefix.take_eq_of_le line 48

Source documentation

Taking the earlier length from a later state recovers the earlier state.

theorem take_eq_of_le (state extra : ℕ → List R)
    (hstep : ∀ n, state (n + 1) = state n ++ extra n)
    {i j : ℕ} (h : i ≤ j) :
    (state j).take ((state i).length) = state i :=
…

theorem OAI.ReflexiveFixedPoints.ListRunPrefix.getElem_eq_of_le line 56
Source documentation
An existing entry has the same value at the same natural index at every later time. The later index bound follows from the proved length inequality.
```
theorem getElem_eq_of_le (state extra : ℕ → List R)
    (hstep : ∀ n, state (n + 1) = state n ++ extra n)
    {i j t : ℕ} (h : i ≤ j) (ht : t < (state i).length) :
    (state j)[t]'(Nat.lt_of_lt_of_le ht (length_le_of_le state extra hstep h)) =
      (state i)[t]'ht :=
…
```
Mentions: OAI.ReflexiveFixedPoints.ListRunPrefix.length_le_of_le