CodeExistence.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Closing the probabilistic segment-code construction at the exact source parameters: block width M² and cutoff ceil(120 log₂ M).

theorem OAI.TreeEdit.BinaryLower.Code.exists_fixed_width_separated_code line 15

Source documentation

A single binary codebook separates all long segments of unequal labels. The alphabet can be arbitrary finite; its size is only bounded by M.

theorem exists_fixed_width_separated_code {M : ℕ} (hM : 2 ≤ M)
    (Γ : Type u) [Fintype Γ] (hΓ : Fintype.card Γ ≤ M) :
    ∃ c : Γ → Word Bool (M ^ 2),
      ∀ (k l : Γ), k ≠ l → ∀ (a i j : ℕ), segmentThreshold M ≤ a →
        i + a ≤ M ^ 2 → j + a ≤ M ^ 2 →
          100 * lcs (((c k).val.drop i).take a)
            (((c l).val.drop j).take a) ≤ 99 * a := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.Code.segmentThreshold, OAI.TreeEdit.lcs

theorem OAI.TreeEdit.BinaryLower.Code.exists_binary_code_with_error_budget line 28

Source documentation

There is an absolute threshold at which the actual codebook and the short-pair error budget needed by the deterministic proof coexist.

theorem exists_binary_code_with_error_budget :
    ∃ M₀ : ℕ, ∀ M : ℕ, M₀ ≤ M →
      2 ≤ M ∧
      2 * (M : ℝ) * segmentThreshold M ≤ (M : ℝ) ^ 2 / 2 ∧
      ∀ (Γ : Type u) [Fintype Γ], Fintype.card Γ ≤ M →
        ∃ c : Γ → Word Bool (M ^ 2),
          ∀ (k l : Γ), k ≠ l → ∀ (a i j : ℕ), segmentThreshold M ≤ a →
            i + a ≤ M ^ 2 → j + a ≤ M ^ 2 →
              100 * lcs (((c k).val.drop i).take a)
                (((c l).val.drop j).take a) ≤ 99 * a := by
…

Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold, OAI.TreeEdit.Word, OAI.TreeEdit.lcs