OAI/NumberTheory/TwoPoint/Walks/ColumnDecoder.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.decodeForestPaths line 18

   Source documentation

   A valid path code determines one family; invalid codes decode to empty lists. The proven uniqueness makes this choice independent of witnesses.

   noncomputable def decodeForestPaths {N segments : ℕ}
       (code : ForestPathData.Code N segments) : Fin segments → List ℕ := by
   …

   Mentions: OAI.TwoPointCorrelations.ForestPathData.Code

2. theorem OAI.TwoPointCorrelations.decodeForestPaths_code line 23
3. inductive OAI.TwoPointCorrelations.CanonicalColumnLabel line 31
4. def OAI.TwoPointCorrelations.evenEntries line 38

   Source documentation

   Incidence supports start with a line and alternate line/point.

   def evenEntries {α : Type*} : List α → List α
     | [] => []
     | [a] => [a]
     | a :: _ :: rest => a :: evenEntries rest
   
   /-- A true bit consumes a regular segment; a false bit consumes one
   omitted run. Unused trailing bits have no effect. -/

5. def OAI.TwoPointCorrelations.mergeColumnRuns line 45

   Source documentation

   A true bit consumes a regular segment; a false bit consumes one omitted run. Unused trailing bits have no effect.

   def mergeColumnRuns {α : Type*} : List Bool → List (List α) → List α → List α
     | [], _, _ => []
     | true :: mask, regular, omitted =>
         regular.headD [] ++ mergeColumnRuns mask regular.tail omitted
     | false :: mask, regular, omitted =>
         omitted.head?.toList ++ mergeColumnRuns mask regular omitted.tail

6. lemma OAI.TwoPointCorrelations.mergeColumnRuns_empty line 52
7. theorem OAI.TwoPointCorrelations.mergeColumnRuns_recover line 60

   Source documentation

   The binary merge data recover any interleaving of regular segments and omitted single runs, including padding to a fixed code length.

   theorem mergeColumnRuns_recover {α : Type*} (pieces : List (List α ⊕ α))
       (padding : List Bool) :
       mergeColumnRuns
         (pieces.map (fun x => match x with | .inl _ => true | .inr _ => false) ++ padding)
         (pieces.filterMap (fun x => match x with | .inl a => some a | .inr _ => none))
         (pieces.filterMap (fun x => match x with | .inl _ => none | .inr a => some a)) =
           pieces.flatMap (fun x => match x with | .inl a => a | .inr a => [a]) := by
   …

   Mentions: OAI.TwoPointCorrelations.mergeColumnRuns

8. def OAI.TwoPointCorrelations.expandColumnRuns line 73

   Source documentation

   The first bit marks an imperfect position; the second begins a new perfect run. Repetition consumes no extra run label.

   def expandColumnRuns : List (Bool × Bool) → List CanonicalColumnLabel →
       Option CanonicalColumnLabel → List (Option CanonicalColumnLabel)
     | [], _, _ => []
     | (true, _) :: flags, runs, _ => none :: expandColumnRuns flags runs none
     | (false, true) :: flags, runs, _ =>
         runs.head? :: expandColumnRuns flags runs.tail runs.head?
     | (false, false) :: flags, runs, previous =>
         previous :: expandColumnRuns flags runs previous

   Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel

9. theorem OAI.TwoPointCorrelations.expandColumnRuns_repeat line 82
10. theorem OAI.TwoPointCorrelations.expandColumnRuns_one_run line 91

    Source documentation

    Positive constant-run lengths are recovered from their boundary bits.

    theorem expandColumnRuns_one_run (n : ℕ) (a : CanonicalColumnLabel)
        (flags : List (Bool × Bool)) (runs : List CanonicalColumnLabel)
        (previous : Option CanonicalColumnLabel) :
        expandColumnRuns ((false, true) :: (List.replicate n (false, false) ++ flags))
            (a :: runs) previous =
          List.replicate (n + 1) (some a) ++ expandColumnRuns flags runs (some a) := by
    …

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

11. theorem OAI.TwoPointCorrelations.expandColumnRuns_length line 100
12. def OAI.TwoPointCorrelations.attachImperfectLabels line 111

    Source documentation

    References to represented perfect labels reuse those labels. A reference to an unrepresented imperfect class uses its first position.

    def attachImperfectLabels (full : List (Option CanonicalColumnLabel)) :
        List (Option CanonicalColumnLabel) → List ℕ → List CanonicalColumnLabel
      | [], _ => []
      | some a :: rest, refs => a :: attachImperfectLabels full rest refs
      | none :: rest, refs =>
          let j := refs.headD 0
    …

    Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel

13. theorem OAI.TwoPointCorrelations.attachImperfectLabels_length line 120
14. abbrev OAI.TwoPointCorrelations.ColumnDecoderCode line 126
15. def OAI.TwoPointCorrelations.decodeColumnLabels line 131
16. theorem OAI.TwoPointCorrelations.decodeColumnLabels_length line 140
17. def OAI.TwoPointCorrelations.decodeColumnPattern line 147

    Source documentation

    An equality pattern contains no numerical label names.

    noncomputable def decodeColumnPattern {N segments omitted imperfect : ℕ}
        (code : ColumnDecoderCode N segments omitted imperfect) : Fin N → Fin N → Bool :=
    …

    Mentions: OAI.TwoPointCorrelations.ColumnDecoderCode

18. theorem OAI.TwoPointCorrelations.card_columnDecoderCode_le line 152
19. theorem OAI.TwoPointCorrelations.card_decoded_column_patterns line 179

    Source documentation

    The decoder's image is one universal, coefficient-independent family of full column equality patterns.

    theorem card_decoded_column_patterns (N segments omitted imperfect : ℕ) :
        Nat.card (Set.range (@decodeColumnPattern N segments omitted imperfect)) ≤
          2 ^ (6 * N + 1) * N ^ (2 * segments + omitted + imperfect) := by
    …

    Mentions: OAI.TwoPointCorrelations.decodeColumnPattern