AlmostLinearConditional.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

An edit-distance approximation scheme conditional on finite scalar Bernstein concentration (Tropp, ACM217, corrected 2023, Theorem 4.16). The same uniform binary algorithm is used in all four clauses.

theorem OAI.EditApproximation.almostLinearEditDistance_conditional line 18

Source documentation

For each fixed binary accuracy in (0,1), the concrete uniform algorithm has success probability at least 2/3, deterministic zero on equal inputs, worst-case expected almost-linear time including preprocessing and sampling, and polynomial space on every outcome. Alphabet bounds are analysis parameters, not inputs to the algorithm. The finite initial range uses exact suffix DP.

theorem almostLinearEditDistance_conditional (epsilon : BinaryFraction)
    (hepsilon : 0 < epsilon.value) (_hepsilonOne : epsilon.value < 1)
    (bernstein : ∀ N, ComputedBernsteinInputs N) :
    (∀ (source target : List ℤ) (N : ℕ), source.length + target.length ≤ N →
      (2 / 3 : ℝ) ≤ (computedFullLaw (source.map integerSymbolCode) (target.map integerSymbolCode) N epsilon).real
        {outcome | EditDistortion.edit source target ≤ integerBinaryAnswer source target N epsilon outcome ∧
          (integerBinaryAnswer source target N epsilon outcome : ℝ) ≤
            (1 + (epsilon.value : ℝ)) * EditDistortion.edit source target}) ∧
    (∀ (source target : List ℤ) (N : ℕ), source = target → ∀ outcome,
      integerBinaryAnswer source target N epsilon outcome = 0) ∧
    (∀ (C : ℕ) (eta : ℝ), 0 < eta → ∀ᶠ N : ℕ in atTop,
      ∀ source target : List ℤ, source.length + target.length ≤ N →
…

Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.ComputedBernsteinInputs, OAI.EditApproximation.computedFullLaw, OAI.EditApproximation.integerSymbolCode, OAI.EditDistortion.edit, OAI.EditApproximation.integerBinaryAnswer

theorem OAI.EditApproximation.integerBinaryAnswer_fallback line 50
Source documentation
The cutoff selects an exact answer, rather than leaving the small-input regime outside the uniform algorithm's correctness statement.
```
theorem integerBinaryAnswer_fallback (source target : List ℤ) (N : ℕ) (epsilon : BinaryFraction)
    (hsmall : ¬ physicalLargeInput N epsilon) (outcome) :
    integerBinaryAnswer source target N epsilon outcome = EditDistortion.edit source target := by
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.physicalLargeInput, OAI.EditApproximation.integerBinaryAnswer, OAI.EditDistortion.edit