TaggedAlignment.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The numeric and list-slice forms of the ordered-tag alignment lemma. These statements allow arbitrary increasing matchings across row boundaries.

theorem OAI.TreeEdit.BinaryLower.Tagged.numeric_alignment_bound line 17

Source documentation

Complete ordered-tag accounting for an arbitrary increasing matching. The local bound counts matches in a whole source/target row pair.

theorem numeric_alignment_bound {L T m B : ℕ} (hm : 2 ≤ m) (hB : 0 < B)
    (u v : Fin L → ℕ) (hu : StrictMono u) (hv : StrictMono v)
    (hub : ∀ i, u i < T * m * B) (hvb : ∀ i, v i < T * m * B)
    (htags : ∀ i, u i / B % m = v i / B % m)
    (d : ℝ) (hd : 0 ≤ d) (hdW : d ≤ (m * B : ℕ))
    (hlocal : ∀ a < T, ∀ b < T,
      ((univ.filter fun i : Fin L =>
        u i / B / m = a ∧ v i / B / m = b).card : ℝ) ≤ (m * B : ℕ) - d) :
    (T : ℝ) * d * (((m - 1) * B : ℕ) : ℝ) /
        (d + (((m - 1) * B : ℕ) : ℝ)) ≤
      (T * m * B : ℕ) - (L : ℝ) := by
…

theorem OAI.TreeEdit.BinaryLower.Tagged.tagged_slice_alignment line 59

Source documentation

Core list version: local row-pair LCS loss and ordered disjoint tags imply the global harmonic lower bound. Slices are literal contiguous rows of width m * B, and all intermediate subsequence matchings remain unrestricted.

theorem tagged_slice_alignment {α : Type*} {T m B : ℕ}
    (hT : 0 < T) (hm : 2 ≤ m) (hB : 0 < B)
    (x y : List α) (hx : x.length = T * m * B) (hy : y.length = T * m * B)
    (htags : ∀ p (hp : p < x.length) q (hq : q < y.length),
      x[p]'hp = y[q]'hq → p / B % m = q / B % m)
    (d : ℝ) (hd : 0 ≤ d)
    (hlocal : ∀ a < T, ∀ b < T,
      (lcs ((x.drop (a * (m * B))).take (m * B))
        ((y.drop (b * (m * B))).take (m * B)) : ℝ) ≤ (m * B : ℕ) - d) :
    (T : ℝ) * d * (((m - 1) * B : ℕ) : ℝ) /
        (d + (((m - 1) * B : ℕ) : ℝ)) ≤
      (deficit (T * m * B) x y : ℝ) := by
…

Mentions: OAI.TreeEdit.lcs, OAI.TreeEdit.BinaryLower.deficit