ColumnRunEncoding.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Reconstructing perfect runs and imperfect attachments from their bits.

theorem OAI.TwoPointCorrelations.mergeColumnRuns_append line 14

Source documentation

Unused segment and reference slots are harmless: they only contribute after the encoded runs have all been emitted.

theorem mergeColumnRuns_append (pieces : List (List α ⊕ α))
    (padding : List Bool) (regularTail : List (List α)) (omittedTail : List α) :
    mergeColumnRuns
      (pieces.map (Sum.elim (fun _ => true) (fun _ => false)) ++ padding)
      (pieces.filterMap (Sum.elim some (fun _ => none)) ++ regularTail)
      (pieces.filterMap (Sum.elim (fun _ => none) some) ++ omittedTail) =
        pieces.flatMap (Sum.elim id List.singleton) ++
          mergeColumnRuns padding regularTail omittedTail := by
…

Mentions: OAI.TwoPointCorrelations.mergeColumnRuns

def OAI.TwoPointCorrelations.columnFlags line 28

Source documentation

Run boundaries reset at imperfect positions.

def columnFlags : List (Option α) → Option α → List (Bool × Bool)
  | [], _ => []
  | none :: rest, _ => (true, false) :: columnFlags rest none
  | some a :: rest, previous =>
      (false, decide (previous ≠ some a)) :: columnFlags rest (some a)

/-- Only the first position of each perfect constant run consumes a label. -/

def OAI.TwoPointCorrelations.columnRunHeads line 35

Source documentation

Only the first position of each perfect constant run consumes a label.

def columnRunHeads : List (Option α) → Option α → List α
  | [], _ => []
  | none :: rest, _ => columnRunHeads rest none
  | some a :: rest, previous =>
      if previous = some a then columnRunHeads rest (some a)
      else a :: columnRunHeads rest (some a)

theorem OAI.TwoPointCorrelations.columnFlags_length line 42
theorem OAI.TwoPointCorrelations.columnRunHeads_length_le line 48
theorem OAI.TwoPointCorrelations.expandColumnRuns_recover line 62
Source documentation
The actual boundary flags and run heads recover every perfect entry.
```
theorem expandColumnRuns_recover (entries : List (Option CanonicalColumnLabel))
    (previous : Option CanonicalColumnLabel) :
    expandColumnRuns (columnFlags entries previous) (columnRunHeads entries previous) previous =
      entries := by
…
```
Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel, OAI.TwoPointCorrelations.expandColumnRuns, OAI.TwoPointCorrelations.columnFlags, OAI.TwoPointCorrelations.columnRunHeads

theorem OAI.TwoPointCorrelations.expandColumnRuns_take_append line 81

Source documentation

Extra code slots cannot affect the entries before the padding boundary.

theorem expandColumnRuns_take_append (flags padding : List (Bool × Bool))
    (runs : List CanonicalColumnLabel) (previous : Option CanonicalColumnLabel) :
    (expandColumnRuns (flags ++ padding) runs previous).take flags.length =
      expandColumnRuns flags runs previous := by
…

Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel, OAI.TwoPointCorrelations.expandColumnRuns

theorem OAI.TwoPointCorrelations.expandColumnRuns_recover_append line 92
Source documentation
Any unused regular-segment labels are ignored by the actual flag prefix.
```
theorem expandColumnRuns_recover_append (entries : List (Option CanonicalColumnLabel))
    (previous : Option CanonicalColumnLabel) (tail : List CanonicalColumnLabel) :
    expandColumnRuns (columnFlags entries previous) (columnRunHeads entries previous ++ tail)
      previous = entries := by
…
```
Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel, OAI.TwoPointCorrelations.expandColumnRuns, OAI.TwoPointCorrelations.columnFlags, OAI.TwoPointCorrelations.columnRunHeads
def OAI.TwoPointCorrelations.markedColumn line 111
Source documentation
Retain labels at perfect positions only.
```
def markedColumn (label : α → CanonicalColumnLabel) (entries : List (α × Bool)) :
    List (Option CanonicalColumnLabel) :=
…
```
Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel
def OAI.TwoPointCorrelations.imperfectColumnReferences line 116
Source documentation
Imperfect positions store one representative each, in their original order.
```
def imperfectColumnReferences (reference : α → ℕ) (entries : List (α × Bool)) : List ℕ :=
…
```
def OAI.TwoPointCorrelations.resolveColumnReference line 120
Source documentation
A reference resolves either to a perfect label or to a fresh imperfect class.
```
def resolveColumnReference (full : List (Option CanonicalColumnLabel)) (j : ℕ) :
    CanonicalColumnLabel := (full[j]?.join).getD (.freshImperfect j)
…
```
Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel

theorem OAI.TwoPointCorrelations.attachImperfectLabels_recover line 126

Source documentation

Correct local representative lookups suffice to recover the whole column, including repetitions across different perfect blocks.

theorem attachImperfectLabels_recover (full : List (Option CanonicalColumnLabel))
    (label : α → CanonicalColumnLabel) (reference : α → ℕ) (entries : List (α × Bool))
    (hreference : ∀ a ∈ entries, a.2 = false →
      resolveColumnReference full (reference a.1) = label a.1) :
    attachImperfectLabels full (markedColumn label entries)
        (imperfectColumnReferences reference entries) = entries.map (fun a => label a.1) := by
…

Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel, OAI.TwoPointCorrelations.resolveColumnReference, OAI.TwoPointCorrelations.attachImperfectLabels, OAI.TwoPointCorrelations.markedColumn, OAI.TwoPointCorrelations.imperfectColumnReferences

theorem OAI.TwoPointCorrelations.attachImperfectLabels_recover_append line 154

Source documentation

Padded flags and references only affect the padded suffix, so a common code universe can accommodate columns shorter than its vertex bound.

theorem attachImperfectLabels_recover_append (full : List (Option CanonicalColumnLabel))
    (label : α → CanonicalColumnLabel) (reference : α → ℕ) (entries : List (α × Bool))
    (padding : List (Option CanonicalColumnLabel)) (referenceTail : List ℕ)
    (hreference : ∀ a ∈ entries, a.2 = false →
      resolveColumnReference full (reference a.1) = label a.1) :
    attachImperfectLabels full (markedColumn label entries ++ padding)
        (imperfectColumnReferences reference entries ++ referenceTail) =
      entries.map (fun a => label a.1) ++ attachImperfectLabels full padding referenceTail := by
…