FixedLengthBinaryConversion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The unconditional prescribed-length binary conversion theorem. The code is selected once for the alphabet and input length, before either input word. The edits used throughout are ordinary unrestricted unit-cost edits.

theorem OAI.TreeEdit.BinaryLower.fixed_length_binary_conversion line 17

Source documentation

Polynomial code, thm:804, including the sharper eq:402 and the exact encoded length. The code is chosen once and works for every input pair.

theorem fixed_length_binary_conversion :
    ∃ M₀ : ℕ, ∀ M : ℕ, M₀ ≤ M →
      ∀ (Γ : Type u) [Fintype Γ],
        1 ≤ Fintype.card Γ → Fintype.card Γ ≤ M →
        ∃ c : Γ → Word Bool (M ^ 2),
          (∀ x : Word Γ M, (encode c x.val).length = M ^ 3) ∧
          ∀ x y : Word Γ M,
            (((M ^ 2 : ℕ) : ℝ) / 804 * (ed x.val y.val : ℝ) ≤
                (ed (encode c x.val) (encode c y.val) : ℝ)) ∧
            ((ed (encode c x.val) (encode c y.val) : ℝ) ≤
                ((M ^ 2 : ℕ) : ℝ) * (ed x.val y.val : ℝ)) ∧
            (((M ^ 2 : ℕ) : ℝ) / 402 * (deficit M x.val y.val : ℝ) ≤
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.encode, OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.deficit