TaggedGaps.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Gap accounting for split rows in ordered-tag alignments.

theorem OAI.TreeEdit.BinaryLower.Tagged.sum_open_gaps line 14

Source documentation

The sum of the open gaps of an increasing matching telescopes.

theorem sum_open_gaps {n : ℕ} (v : Fin (n + 1) → ℕ) :
    (∑ i : Fin n, ((v i.succ : ℝ) - (v i.castSucc : ℝ) - 1)) =
      (v (Fin.last n) : ℝ) - (v 0 : ℝ) - n := by
…

theorem OAI.TreeEdit.BinaryLower.Tagged.selected_gap_bound line 25

Source documentation

Chosen disjoint gaps cannot exceed the total number of unmatched target positions. No assumption about aligned row boundaries is made.

theorem selected_gap_bound {n N : ℕ} (v : Fin (n + 1) → ℕ)
    (hv : StrictMono v) (hN : ∀ i, v i < N) (S : Finset (Fin n))
    (g : ℝ) (hg : ∀ i ∈ S, g ≤ (v i.succ : ℝ) - (v i.castSucc : ℝ) - 1) :
    (S.card : ℝ) * g ≤ (N : ℝ) - (n + 1) := by
…

theorem OAI.TreeEdit.BinaryLower.Tagged.tag_le_of_same_row line 49
Source documentation
Equal row indices force the ordered tags of two source positions to be nondecreasing.
```
theorem tag_le_of_same_row {a b m B : ℕ} (hab : a ≤ b)
    (hrow : a / B / m = b / B / m) :
    (a / B) % m ≤ (b / B) % m := by
…
```

theorem OAI.TreeEdit.BinaryLower.Tagged.tagged_gap line 60

Source documentation

A transition to a later target row, while staying in one source row, forces at least (m-1)*B skipped target positions.

theorem tagged_gap {a b c d m B : ℕ} (hm : 1 ≤ m) (hB : 0 < B)
    (hab : a ≤ b) (hsource : a / B / m = b / B / m)
    (htarget : c / B / m < d / B / m)
    (htag₀ : (a / B) % m = (c / B) % m)
    (htag₁ : (b / B) % m = (d / B) % m) :
    c + 1 + (m - 1) * B ≤ d := by
…

def OAI.TreeEdit.BinaryLower.Tagged.splitTransitions line 88
Source documentation
Consecutive matching entries that cross a target-row boundary without crossing a source-row boundary.
```
def splitTransitions {n : ℕ} (m B : ℕ) (u v : Fin (n + 1) → ℕ) :
    Finset (Fin n) :=
…
```
def OAI.TreeEdit.BinaryLower.Tagged.splitRows line 94
Source documentation
Source rows which contain such a transition.
```
def splitRows {n : ℕ} (m B : ℕ) (u v : Fin (n + 1) → ℕ) : Finset ℕ :=
…
```

theorem OAI.TreeEdit.BinaryLower.Tagged.constant_on_row_fiber line 99

Source documentation

For a monotone row map, equality on adjoining entries in a row implies equality throughout that row's matching fiber.

theorem constant_on_row_fiber {n : ℕ} (R S : Fin (n + 1) → ℕ)
    (hR : Monotone R) (r : ℕ)
    (hstep : ∀ i : Fin n, R i.castSucc = r → R i.succ = r →
      S i.castSucc = S i.succ) :
    ∀ i j, R i = r → R j = r → S i = S j := by
…

theorem OAI.TreeEdit.BinaryLower.Tagged.target_row_eq_of_not_split line 136

Source documentation

A row not counted as split sends all its matches to one target row.

theorem target_row_eq_of_not_split {n m B r : ℕ}
    (u v : Fin (n + 1) → ℕ) (hu : Monotone u)
    (hr : r ∉ splitRows m B u v) :
    ∀ i j, u i / B / m = r → u j / B / m = r →
      v i / B / m = v j / B / m := by
…

Mentions: OAI.TreeEdit.BinaryLower.Tagged.splitRows

theorem OAI.TreeEdit.BinaryLower.Tagged.mem_splitRows_iff line 151

Source documentation

The transition definition counts exactly the rows with matches in two distinct target rows.

theorem mem_splitRows_iff {n m B r : ℕ}
    (u v : Fin (n + 1) → ℕ) (hu : Monotone u) :
    r ∈ splitRows m B u v ↔
      ∃ i j, u i / B / m = r ∧ u j / B / m = r ∧
        v i / B / m ≠ v j / B / m := by
…

Mentions: OAI.TreeEdit.BinaryLower.Tagged.splitRows

theorem OAI.TreeEdit.BinaryLower.Tagged.row_index_lt line 166
Source documentation
Row indices of positions in a T-row word are strictly below T.
```
theorem row_index_lt {p T m B : ℕ} (hm : 0 < m) (hB : 0 < B)
    (hp : p < T * m * B) : p / B / m < T := by
…
```
theorem OAI.TreeEdit.BinaryLower.Tagged.splitRows_subset_range line 172
theorem OAI.TreeEdit.BinaryLower.Tagged.card_fin_rows line 181
Source documentation
Passing a set of valid natural row indices to Fin T preserves its cardinality.
```
theorem card_fin_rows {T : ℕ} (S : Finset ℕ) (hS : S ⊆ range T) :
    (univ.filter fun r : Fin T => r.val ∈ S).card = S.card := by
…
```

theorem OAI.TreeEdit.BinaryLower.Tagged.nonsplit_row_card_le line 196

Source documentation

Per-row-pair matching bounds apply to every nonsplit source row. Empty source fibers are included rather than discarded.

theorem nonsplit_row_card_le {n T m B : ℕ} (hm : 0 < m) (hB : 0 < B)
    (u v : Fin (n + 1) → ℕ) (hu : Monotone u)
    (hv : ∀ i, v i < T * m * B) (d : ℝ) (hd : d ≤ (m * B : ℕ))
    (hlocal : ∀ a < T, ∀ b < T,
      ((univ.filter fun i : Fin (n + 1) =>
        u i / B / m = a ∧ v i / B / m = b).card : ℝ) ≤ (m * B : ℕ) - d)
    {a : ℕ} (ha : a < T) (haS : a ∉ splitRows m B u v) :
    ((univ.filter fun i : Fin (n + 1) => u i / B / m = a).card : ℝ) ≤
      (m * B : ℕ) - d := by
…

Mentions: OAI.TreeEdit.BinaryLower.Tagged.splitRows

theorem OAI.TreeEdit.BinaryLower.Tagged.split_rows_gap_bound line 228

Source documentation

The split-row inequality, with no restriction on how many times a source row crosses target rows.

theorem split_rows_gap_bound {n N m B : ℕ} (hm : 1 ≤ m) (hB : 0 < B)
    (u v : Fin (n + 1) → ℕ) (hu : StrictMono u) (hv : StrictMono v)
    (hN : ∀ i, v i < N)
    (htags : ∀ i, (u i / B) % m = (v i / B) % m) :
    ((splitRows m B u v).card : ℝ) * (((m - 1) * B : ℕ) : ℝ) ≤
      (N : ℝ) - (n + 1) := by
…

Mentions: OAI.TreeEdit.BinaryLower.Tagged.splitRows

theorem OAI.TreeEdit.BinaryLower.Tagged.harmonic_bound line 260
Source documentation
The algebraic conclusion of the split and nonsplit accounts, including zero local deficit.
```
theorem harmonic_bound {E d g T s : ℝ} (hd : 0 ≤ d) (hg : 0 < g)
    (hunsplit : d * (T - s) ≤ E) (hsplit : s * g ≤ E) :
    T * d * g / (d + g) ≤ E := by
…
```
theorem OAI.TreeEdit.BinaryLower.Tagged.half_min_le_harmonic line 270
Source documentation
The harmonic lower bound implies the convenient half-minimum form.
```
theorem half_min_le_harmonic {d g T : ℝ} (hd : 0 ≤ d) (hg : 0 < g)
    (hT : 0 ≤ T) :
    T / 2 * min d g ≤ T * d * g / (d + g) := by
…
```
theorem OAI.TreeEdit.BinaryLower.Tagged.harmonic_le_total line 285
Source documentation
Empty matchings satisfy the same bound, using only the evident local upper bound on the row deficit.
```
theorem harmonic_le_total {T d g W : ℝ} (hT : 0 ≤ T) (hd : 0 ≤ d)
    (hg : 0 < g) (hdW : d ≤ W) :
    T * d * g / (d + g) ≤ T * W := by
…
```

theorem OAI.TreeEdit.BinaryLower.Tagged.half_local_le_harmonic line 297

Source documentation

The commonly used Td/2 consequence, with its actual hypothesis.

theorem half_local_le_harmonic {d g T : ℝ} (hd : 0 ≤ d) (hg : 0 < g)
    (hT : 0 ≤ T) (hdg : d ≤ g) :
    T * d / 2 ≤ T * d * g / (d + g) := by
…