CanonicalColumnEncoding.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Occurrence representatives recover all equalities involving imperfect positions.

theorem OAI.TwoPointCorrelations.reference_filterMap_length line 10

theorem OAI.TwoPointCorrelations.canonical_column_encoding line 23

Source documentation

Once the regular-path and omitted-run geometry is encoded, all remaining positions use their proved canonical representatives; no reference lookup or equality-pattern reconstruction hypothesis is needed.

theorem canonical_column_encoding {α : Type*} [DecidableEq α]
    {n N segments omitted imperfect : ℕ} (hN : 0 < N) (hn : n ≤ N)
    (label : Fin n → α) (perfect : Finset (Fin n)) (name : Fin n → ℕ ⊕ ℕ)
    (pathCode : ForestPathData.Code N segments)
    (cuts : List (Option CanonicalColumnLabel × Bool))
    (hcuts : cuts.map Prod.fst = canonicalPerfectEntries label perfect name)
    (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) =
        pieces.filterMap (Sum.elim some (fun _ => none)) ++ regularTail)
…

Mentions: OAI.TwoPointCorrelations.ForestPathData.Code, OAI.TwoPointCorrelations.CanonicalColumnLabel, OAI.TwoPointCorrelations.canonicalPerfectEntries, OAI.TwoPointCorrelations.evenEntries, OAI.TwoPointCorrelations.decodeForestPaths