def Hex.GraphIso.Nauty.Sparse.Sort.children (start size left right : Nat) (rest : List (Nat × Nat)) : List (Nat × Nat)

The exact two pushes in the indirect sort, with the smaller fragment at the top of the stack. Fragments of size at most one need no work.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.Sort.weight (stack : List (Nat × Nat)) : Nat

Total length of the pending segments.

Equations

• Hex.GraphIso.Nauty.Sparse.Sort.weight stack = (List.map Prod.snd stack).sum

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.Sort.weight_nil : weight [] = 0

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.Sort.weight_cons (p : Nat × Nat) (rest : List (Nat × Nat)) : weight (p :: rest) = p.snd + weight rest

theorem Hex.GraphIso.Nauty.Sparse.Sort.children_weight (start size left right : Nat) (rest : List (Nat × Nat)) : weight (children start size left right rest) ≤ left + right + weight rest

theorem Hex.GraphIso.Nauty.Sparse.Sort.children_bounds (start size left right bound : Nat) (rest : List (Nat × Nat)) (hb : start + size ≤ bound) (hl : left ≤ size) (hr : right ≤ size) (hs : ∀ (p : Nat × Nat), p ∈ rest → 1 < p.snd ∧ p.fst + p.snd ≤ bound) (p : Nat × Nat) : p ∈ children start size left right rest → 1 < p.snd ∧ p.fst + p.snd ≤ bound

theorem Hex.GraphIso.Nauty.Sparse.Sort.indirect_induction (x y : Array Nat) (start len : Nat) (hb : start + len ≤ x.size) (P : Array Nat → List (Nat × Nat) → Prop) (hinit : P x (if len > 1 then [(start, len)] else [])) (hins : ∀ (a : Array Nat) (lo size : Nat) (rest : List (Nat × Nat)), a.size = x.size → lo + size ≤ x.size → size < 11 → P a ((lo, size) :: rest) → P (insertion a y lo size) rest) (hpart : ∀ (a : Array Nat) (lo size : Nat) (rest : List (Nat × Nat)), a.size = x.size → lo + size ≤ x.size → 11 ≤ size → P a ((lo, size) :: rest) → P (partition a y lo size).fst (children lo size (partition a y lo size).snd.fst (partition a y lo size).snd.snd rest)) : P (indirect x y start len) []

Induction over the actual bounded work-stack loop. A property preserved by its insertion and partition steps holds with an empty final stack: the loop bound cannot truncate pending work on a valid input segment.

theorem Hex.GraphIso.Nauty.Sparse.Sort.indirect_outside (x y : Array Nat) (start len q : Nat) (hb : start + len ≤ x.size) (hq : q < start ∨ start + len ≤ q) : (indirect x y start len)[q]! = x[q]!

The full indirect sort changes only entries in the requested segment.

theorem Hex.GraphIso.Nauty.Sparse.Sort.extract_eq {a b : Array Nat} (hs : a.size = b.size) (lo hi : Nat) (he : ∀ (q : Nat), lo ≤ q → q < hi → a[q]! = b[q]!) : a.extract lo hi = b.extract lo hi

theorem Hex.GraphIso.Nauty.Sparse.Sort.split_three (a : Array Nat) (lo hi bound : Nat) (hlo : lo ≤ hi) (hhi : hi ≤ bound) (ha : a.size = bound) : a.extract 0 lo ++ a.extract lo hi ++ a.extract hi bound = a

theorem Hex.GraphIso.Nauty.Sparse.Sort.indirect_segment (x y : Array Nat) (start len : Nat) (hb : start + len ≤ x.size) : ((indirect x y start len).extract start (start + len)).toList.Perm (x.extract start (start + len)).toList

Permutation preservation holds for the segment itself, with the unchanged prefix and suffix cancelled from the whole-array permutation.