HexGraphIso.Nauty.Sparse.IndexRuns

structure Hex.GraphIso.Nauty.Sparse.Index.Run (lab hits : Array Nat) (first last a b : Nat) :

A maximal constant-count run inside one original cell. Both endpoints are inclusive, as in the cached endpoint array.

Instances For

theorem Hex.GraphIso.Nauty.Sparse.Index.Run.disjoint_or_eq {lab hits : Array Nat} {first last a b a' b' : Nat} (h : Run lab hits first last a b) (h' : Run lab hits first last a' b') :

b < a' ∨ b' < a ∨ a = a' ∧ b = b'

theorem Hex.GraphIso.Nauty.Sparse.Index.Run.cell {level first last : Nat} {lab hits before ptn : Array Nat} {a b : Nat} (h : CountPartition level first last lab hits before ptn) (hc : IsCell before level first (last + 1 - first)) (ha : first ≤ a) (hab : a ≤ b) (hb : b ≤ last) :

IsCell ptn level a (b + 1 - a) ↔ Run lab hits first last a b

structure Hex.GraphIso.Nauty.Sparse.Index.Runs (n first last upto : Nat) (lab hits starts ends : Array Nat) :

Cache entries for the completed runs of a count split. This invariant does not require the next run's boundary to have been written yet.

starts_size : starts.size = n
ends_size : ends.size = n
ends_eq (a b : Nat) : Run lab hits first last a b → b < upto → ends[a]! = b
starts_eq (a b : Nat) : Run lab hits first last a b → b < upto → ∀ (q : Nat), a ≤ q → q ≤ b → starts[lab[q]!]! = if a = b then n else a

Instances For

theorem Hex.GraphIso.Nauty.Sparse.Index.Runs.of_first {n first last b : Nat} {lab hits starts ends : Array Nat} (hr : Run lab hits first last first b) (hb : b < n) (hs : starts.size = n) (he : ends.size = n) (hv : ∀ (q : Nat), first ≤ q → q ≤ b → starts[lab[q]!]! = if first = b then n else first) :

Runs n first last (b + 1) lab hits starts (ends.setIfInBounds first b)

The first completed run has no earlier run to preserve.

theorem Hex.GraphIso.Nauty.Sparse.Index.Runs.initial {n first last : Nat} {lab hits starts ends : Array Nat} (hs : starts.size = n) (he : ends.size = n) :

Runs n first last first lab hits starts ends

theorem Hex.GraphIso.Nauty.Sparse.Index.Runs.extend {n first last a b : Nat} {lab hits starts ends out : Array Nat} (h : Runs n first last a lab hits starts ends) (hr : Run lab hits first last a b) (hb : b < n) (hs : out.size = n) (ho : ∀ (q : Nat), q < n → out[lab[q]!]! = if a ≤ q ∧ q ≤ b then if a = b then n else a else starts[lab[q]!]!) :

Runs n first last (b + 1) lab hits out (ends.setIfInBounds a b)

Scattering one whole run preserves every preceding run's entries and extends the completed prefix through the newly stored endpoint.

theorem Hex.GraphIso.Nauty.Sparse.Index.Scatter.prepend {n : Nat} {lab before after : Array Nat} {a b : Nat} (h : Scatter n lab before after (a + 1) (b + 1) a) (hbound : ∀ (i : Nat), i < n → lab[i]! < n) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hab : a ≤ b) (hb : b < n) :

Scatter n lab before (after.setIfInBounds lab[a]! (if a = b then n else a)) a (b + 1) (if a = b then n else a)

The tail scan writes positions after the run's first vertex. The final first-vertex write completes that scatter, with the singleton sentinel.

theorem Hex.GraphIso.Nauty.Sparse.Minima.first_run {lab hits : Array Nat} {first v2 v3 last w1 w2 : Nat} (h : Minima lab hits first v2 v3 last w1 w2) (hv : v2 < v3) :

Index.Run lab hits first (last - 1) first (v2 - 1)

theorem Hex.GraphIso.Nauty.Sparse.Minima.second_run {lab hits : Array Nat} {first v2 v3 last w1 w2 : Nat} (h : Minima lab hits first v2 v3 last w1 w2) (hv : v2 < v3) :

Index.Run lab hits first (last - 1) v2 (v3 - 1)