ColumnPieceMembership.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Membership information retained by the actual perfect-block cut.

theorem OAI.TwoPointCorrelations.columnChunkEntries_map line 13
theorem OAI.TwoPointCorrelations.columnRunHeads_mem_original line 23

theorem OAI.TwoPointCorrelations.columnChunkPieces_regular_membership line 30

Source documentation

A regular piece retains both its regular status and a genuinely perfect occurrence in the original column.

theorem columnChunkPieces_regular_membership (omitted : α → Bool)
    (chunks : List (List α ⊕ α)) (segment : List α)
    (hs : Sum.inl segment ∈ columnChunkPieces omitted chunks) :
    segment ≠ [] ∧ ∀ a ∈ segment, omitted a = false ∧ (a, true) ∈ columnChunkEntries chunks := by
…

Mentions: OAI.TwoPointCorrelations.columnChunkPieces, OAI.TwoPointCorrelations.columnChunkEntries

theorem OAI.TwoPointCorrelations.columnChunkPieces_omitted_membership line 49
Source documentation
Omitted runs also come from perfect positions; their separate names therefore fit within the original occurrence-index bound.
```
theorem columnChunkPieces_omitted_membership (omitted : α → Bool)
    (chunks : List (List α ⊕ α)) (a : α)
    (ha : Sum.inr a ∈ columnChunkPieces omitted chunks) :
    omitted a = true ∧ (a, true) ∈ columnChunkEntries chunks := by
…
```
Mentions: OAI.TwoPointCorrelations.columnChunkPieces, OAI.TwoPointCorrelations.columnChunkEntries

theorem OAI.TwoPointCorrelations.omitted_names_lift line 67

Source documentation

A bounded list of omitted canonical names has an equally long list of decoder indices, so no extra naming cost is introduced.

theorem omitted_names_lift {N : ℕ} (names : List CanonicalColumnLabel)
    (h : ∀ a ∈ names, ∃ j : Fin N, a = .omitted j.val) :
    ∃ indices : List (Fin N), indices.length = names.length ∧
      indices.map (fun j => CanonicalColumnLabel.omitted j.val) = names := by
…

Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel