OAI/NumberTheory/TwoPoint/Walks/ColumnEncodingRealization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.columnPieceMask line 10
2. def OAI.TwoPointCorrelations.columnPieceRegular line 13
3. def OAI.TwoPointCorrelations.columnPieceOmitted line 17
4. def OAI.TwoPointCorrelations.columnPieceFlatten line 21
5. theorem OAI.TwoPointCorrelations.resolveColumnReference_append line 25
6. theorem OAI.TwoPointCorrelations.column_encoding_realization line 33

   Source documentation

   The geometric inputs are exact regular path lists and an interleaving of regular segments with omitted runs. No full equality-pattern or decoder conclusion is assumed. All unused slots may be padded independently.

   theorem column_encoding_realization {α : Type*} {N segments omitted imperfect : ℕ} (hN : 0 < N)
       (name : α → CanonicalColumnLabel)
       (pathCode : ForestPathData.Code N segments)
       (entries : List (α × Bool)) (hentries : entries.length ≤ N)
       (cuts : List (Option CanonicalColumnLabel × Bool))
       (hcuts : cuts.map Prod.fst = markedColumn name entries)
       (pieces : List (List CanonicalColumnLabel ⊕ CanonicalColumnLabel))
       (hpieces : pieces.length ≤ N)
       (regularTail : List (List CanonicalColumnLabel))
       (hregular : List.ofFn (fun i => (evenEntries (decodeForestPaths pathCode i)).map CanonicalColumnLabel.regular) =
         columnPieceRegular pieces ++ regularTail)
       (omittedNames : List (Fin N)) (homittedSize : omittedNames.length ≤ omitted)
   …

   Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel, OAI.TwoPointCorrelations.ForestPathData.Code, OAI.TwoPointCorrelations.markedColumn, OAI.TwoPointCorrelations.evenEntries, OAI.TwoPointCorrelations.decodeForestPaths, OAI.TwoPointCorrelations.columnPieceRegular