def Hex.GraphIso.Nauty.Sparse.Target.encode (keys : List Nat) (n k : Nat) : Nat

Translate a cached cell start into the fresh selector's compact index, retaining the singleton sentinel.

Equations

• Hex.GraphIso.Nauty.Sparse.Target.encode keys n k = if k = n then n else List.idxOf k keys

theorem Hex.GraphIso.Nauty.Sparse.Target.encode_lt {keys : List Nat} {n k : Nat} (hn : ¬n ∈ keys) (hlen : keys.length ≤ n) (hk : k ∈ keys) : encode keys n k < n

theorem Hex.GraphIso.Nauty.Sparse.Target.encode_eq_iff {keys : List Nat} {n a b : Nat} (hn : ¬n ∈ keys) (hlen : keys.length ≤ n) (ha : a ∈ keys) (hb : b = n ∨ b ∈ keys) : encode keys n b = encode keys n a ↔ b = a

The compact encoding is injective on all entries that a row can contain.

theorem Hex.GraphIso.Nauty.Sparse.Target.count_encode {keys row : List Nat} {n a : Nat} (hn : ¬n ∈ keys) (hlen : keys.length ≤ n) (ha : a ∈ keys) (hr : ∀ (v : Nat), v ∈ row → v = n ∨ v ∈ keys) : List.count (encode keys n a) (List.map (encode keys n) row) = List.count a row

A row has the same number of incidences with a cell in either encoding.

theorem Hex.GraphIso.Nauty.Sparse.Target.range_get (keys : List Nat) : List.map (fun (i : Nat) => keys[i]!) (List.range keys.length) = keys

theorem Hex.GraphIso.Nauty.Sparse.Target.scores_encode {keys row : List Nat} {n : Nat} {rankSize degree : Nat → Nat} (hn : keys.Nodup) (hsentinel : ¬n ∈ keys) (hlen : keys.length ≤ n) (hr : ∀ (v : Nat), v ∈ row → v = n ∨ v ∈ keys) (hs : ∀ (i : Nat), i < keys.length → rankSize i = degree keys[i]!) : List.countP (Join.qualifies (List.map (encode keys n) row) rankSize) (List.range keys.length) = List.countP (Join.qualifies row degree) keys

Compact-index join counts equal the counts over actual cell starts.