SegmentCode.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite probabilistic construction of a codebook simultaneously separating every long segment of every pair of differently labelled blocks. Counting is done on all Boolean codebooks, so no randomness or existence hypothesis is retained.

def OAI.TreeEdit.BinaryLower.SegmentCode.window line 18
Source documentation
A contiguous window of positions in a block.
```
def window {P : ℕ} (a i : ℕ) (h : i+a ≤ P) : Fin a → Fin P :=
…
```
theorem OAI.TreeEdit.BinaryLower.SegmentCode.window_injective line 21
def OAI.TreeEdit.BinaryLower.SegmentCode.SegmentSeparated line 30
Source documentation
Segment separation in terms of increasing position lists.
```
def SegmentSeparated {K P : ℕ} (c : Fin K → Fin P → Bool) (a₀ : ℕ) : Prop :=
…
```
def OAI.TreeEdit.BinaryLower.SegmentCode.comparisonBad line 38
Source documentation
Bad comparisons include only valid windows longer than the cutoff.
```
noncomputable def comparisonBad {K P : ℕ} (a₀ : ℕ)
    (t : SegmentComparison K (P+1)) : Finset (Fin K → Fin P → Bool) := by
…
```
theorem OAI.TreeEdit.BinaryLower.SegmentCode.comparisonBad_fraction_le line 48
Source documentation
Each valid comparison has exponentially small bad-event frequency.
```
theorem comparisonBad_fraction_le {K P : ℕ} (a₀ : ℕ)
    (t : SegmentComparison K (P+1)) :
    ((comparisonBad a₀ t).card : ℝ) / Fintype.card (Fin K → Fin P → Bool) ≤
      (9/10 : ℝ)^a₀ := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.SegmentCode.comparisonBad
theorem OAI.TreeEdit.BinaryLower.SegmentCode.exists_segmentSeparated line 79
Source documentation
A finite numerical union-bound criterion produces one codebook that works for every pair of labels, every valid pair of windows, and every matching.
```
theorem exists_segmentSeparated (K P a₀ : ℕ)
    (hprob : (K : ℝ)^2 * ((P+1 : ℕ) : ℝ)^3 * (9/10 : ℝ)^a₀ < 1) :
    ∃ c : Fin K → Fin P → Bool, SegmentSeparated c a₀ := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.SegmentCode.SegmentSeparated