structure Hex.GraphIso.Nauty.Sparse.Target.MapPrefix (n : Nat) (lab cache : Array Nat) (keys : List Nat) (upto : Nat) (raw : Array Nat) : Prop

The compact-index map is installed through upto; untouched vertices retain the singleton sentinel from the initial allocation.

• size : raw.size = n
• get (i : Nat) : i < n → raw[lab[i]!]! = if i < upto then encode keys n cache[lab[i]!]! else n

theorem Hex.GraphIso.Nauty.Sparse.Target.MapPrefix.initial {n : Nat} {lab cache : Array Nat} (keys : List Nat) (hb : ∀ (i : Nat), i < n → lab[i]! < n) : MapPrefix n lab cache keys 0 (Array.replicate n n)

theorem Hex.GraphIso.Nauty.Sparse.Target.MapPrefix.advance {n first last value : Nat} {lab cache raw out : Array Nat} {keys : List Nat} (h : MapPrefix n lab cache keys first raw) (hscatter : Index.Scatter n lab raw out first (last + 1) value) (horder : first ≤ last) (hv : ∀ (i : Nat), first ≤ i → i ≤ last → encode keys n cache[lab[i]!]! = value) : MapPrefix n lab cache keys (last + 1) out

Installing one nontrivial cell extends the map without changing earlier vertices; the source performs exactly this scatter with its compact index.

theorem Hex.GraphIso.Nauty.Sparse.Target.MapPrefix.set {n i value : Nat} {lab cache raw : Array Nat} {keys : List Nat} (h : MapPrefix n lab cache keys i raw) (hi : i < n) (hbound : ∀ (j : Nat), j < n → lab[j]! < n) (hinj : ∀ (a b : Nat), a < n → b < n → lab[a]! = lab[b]! → a = b) (hv : value = encode keys n cache[lab[i]!]!) : MapPrefix n lab cache keys (i + 1) (raw.set! lab[i]! value)

One executed scatter assignment extends the installed positional prefix.

theorem Hex.GraphIso.Nauty.Sparse.Target.MapPrefix.singleton {n first : Nat} {lab cache raw : Array Nat} {keys : List Nat} (h : MapPrefix n lab cache keys first raw) (hc : cache[lab[first]!]! = n) : MapPrefix n lab cache keys (first + 1) raw

A singleton needs no write: its unchanged sentinel is already correct.

theorem Hex.GraphIso.Nauty.Sparse.Target.MapPrefix.finish {n upto : Nat} {lab cache raw : Array Nat} {keys : List Nat} (h : MapPrefix n lab cache keys upto raw) (hu : n ≤ upto) : MapPrefix n lab cache keys n raw

A cursor beyond the vertex range has installed every position.

theorem Hex.GraphIso.Nauty.Sparse.Target.MapPrefix.complete {n : Nat} {lab cache raw : Array Nat} {keys : List Nat} (h : MapPrefix n lab cache keys n raw) (l : Label n) (hl : Label.ofArray? n lab = some l) (v : Fin n) : raw[↑v]! = encode keys n cache[↑v]!

The completed scatter agrees with the compact encoding on every vertex, using the checked label's inverse to recover its unique position.