OAI/NumberTheory/TwoPoint/Walks/ColumnBoundaryEncoding.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Run bits may force a split at a perfect-block boundary without changing its label.

  1. def OAI.TwoPointCorrelations.columnFlagsWithCuts line 11
  2. def OAI.TwoPointCorrelations.columnRunHeadsWithCuts line 17
  3. theorem OAI.TwoPointCorrelations.columnFlagsWithCuts_length line 24
  4. theorem OAI.TwoPointCorrelations.expandColumnRuns_cuts_recover line 32

    Source documentation

    A forced boundary consumes a run label even when the adjacent blocks end and start with the same label. Arbitrary unused labels remain harmless.

    theorem expandColumnRuns_cuts_recover (entries : List (Option CanonicalColumnLabel × Bool))
    (previous : Option CanonicalColumnLabel) (tail : List CanonicalColumnLabel) :
    expandColumnRuns (columnFlagsWithCuts entries previous)
      (columnRunHeadsWithCuts entries previous ++ tail) previous = entries.map Prod.fst := by
…

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