theorem
Hex.GraphIso.Nauty.isCell_breakout_target
{n : Nat}
{lab ptn : Array Nat}
{level tc tv : Nat}
(hlt : tc < ptn.size)
(hstart : tc = 0 ∨ ptn[tc - 1]! ≤ level)
:
Individualizing closes the target position, so it becomes a singleton cell one level down. This is what makes the transport below apply from the child onwards.
theorem
Hex.GraphIso.Nauty.refine_fixes_singleton
{n : Nat}
{ctx : Ctx n}
{level : Nat}
{lab ptn : Array Nat}
{active : VSet n}
{numcells a : Nat}
(hnn : n ≤ ptn.size)
(hs : lab.size = ptn.size)
(hend : ptn[ptn.size - 1]! ≤ level)
(hc : IsCell ptn level a 1)
:
refine leaves a singleton cell's position exactly where it was:
it permutes cell contents, and a singleton cell has only one.
theorem
Hex.GraphIso.Nauty.breakout_misses_singleton
{n : Nat}
{lab ptn : Array Nat}
{level a tc o : Nat}
(hinj : LabInj lab lab.size)
(hto : tc + o < lab.size)
(hout : a < tc ∨ tc + o < a)
:
A breakout at a different cell leaves a singleton cell's position
alone. Together with refine_fixes_singleton this is the whole content
of the descent's position bookkeeping, one operation at a time.
theorem
Hex.GraphIso.Nauty.isCell_refine_one
{n : Nat}
{ctx : Ctx n}
{level : Nat}
{active : VSet n}
{numcells a : Nat}
{lab ptn : Array Nat}
(hnn : n = ptn.size)
(hls : lab.size = ptn.size)
(hend : ptn[ptn.size - 1]! ≤ level)
(hc : IsCell ptn level a 1)
:
Refinement preserves an existing singleton cell.