theorem
Hex.GraphIso.Nauty.Sparse.Minima.Permuted.indices
{lab : Array Nat}
{first last v2 v3 w1 w2 cap n : Nat}
{s : RefineSt n}
(hm : Permuted s.lab lab s.hits first last v2 v3 last w1 w2 cap)
(hp : s.lab.toList.Perm (List.range n))
(hb : last ≤ n)
(hs : s.cellstart.size = n)
(hc : ∀ (q : Nat), first ≤ q → q < last → s.cellstart[s.lab[q]!]! = first)
:
The first-fragment singleton write initializes the two-fragment index invariant without disturbing any cell outside the split.
theorem
Hex.GraphIso.Nauty.Sparse.Minima.Permuted.indices_single
{lab : Array Nat}
{first last v2 v3 w1 w2 cap n : Nat}
{s : RefineSt n}
(hm : Permuted s.lab lab s.hits first last v2 v3 last w1 w2 cap)
(hp : s.lab.toList.Perm (List.range n))
(hb : last ≤ n)
(hs : s.cellstart.size = n)
(hc : ∀ (q : Nat), first ≤ q → q < last → s.cellstart[s.lab[q]!]! = first)
(hv : v3 = v2 + 1)
:
The singleton second fragment uses one sentinel write instead of the scatter loop, preserving the same completed-run contract.
theorem
Hex.GraphIso.Nauty.Sparse.Index.Two.set_long
{n first v2 v3 upto : Nat}
{lab starts : Array Nat}
{last : Nat}
{oldlab oldstarts oldends ends : Array Nat}
(ht : Two n first v2 v3 upto lab starts)
(hf : Frame n first last oldlab lab oldstarts starts oldends ends)
(hp : lab.toList.Perm (List.range n))
(hfirst : first ≤ upto)
(hu : v2 ≤ upto)
(hlast : upto ≤ last)
(hb : upto < n)
(hv : v3 ≠ v2 + 1)
:
A second-fragment scatter write preserves both earlier fragment entries and all entries outside the original cell.