theorem
Hex.GraphIso.Nauty.Max.Scope.stab_below
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level : Nat}
{cs bs : List Nat}
{st : Search n}
{parents : Parents n}
(h : Scope G ctx tcLevel level cs bs st parents)
{a b : Nat}
{p q : Parent n}
{γ : Array Nat}
(hp : parents a = some p)
(hq : parents b = some q)
(hab : a ≤ b)
(hs : CellStab q.state.ptn b q.state.lab γ)
:
A permutation stabilizing a saved target frame stabilizes every coarser saved ancestor. Their effects into the same current state supply both the cell-content transport and the boundary inclusion.
theorem
Hex.GraphIso.Nauty.Max.Parent.reindex_stab
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{p : Parent n}
(h : Valid G ctx tcLevel p)
{γ : Array Nat}
(hs :
CellStab (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.ptn p.loop.node.level
(Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.lab γ)
:
The actual target-frame ordering has the same stabilization relation as the frozen sweep ordering.
theorem
Hex.GraphIso.Nauty.Max.Parent.scatter_stab
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{p : Parent n}
(h : Valid G ctx tcLevel p)
{ref lab γ : Array Nat}
(href : ref.size = n)
(hfr :
cellsPerm (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.ptn p.loop.node.level
(Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.lab ref)
(hl :
cellsPerm (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.ptn p.loop.node.level
(Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.lab lab)
(hmap : ∀ (i : Nat), i < n → γ[ref[i]!]! = lab[i]!)
:
A reference scatter stabilizes the actual saved parent partition.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.first_stab
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel false f bs fs parents)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hauto :
have p := prepareOther ctx tcLevel f.level f.numcells f.entry;
(classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoFirst)
{p : Parent n}
(hp : parents f.entry.gcaFirst = some p)
:
Code one's scatter stabilizes its saved first ancestor.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.canon_stab
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel false f bs fs parents)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hauto :
have p := prepareOther ctx tcLevel f.level f.numcells f.entry;
(classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon)
{p : Parent n}
(hp : parents f.entry.gcaCanon = some p)
:
Code two's scatter stabilizes its saved canonical ancestor.