def Hex.GraphIso.Nauty.Max.Parents.push {n : Nat} (parents : Parents n) (p : Parent n) : Parents n

Save the parent being suspended by the next child call.

Equations

• parents.push p level = if level = p.loop.node.level then some p else parents level

theorem Hex.GraphIso.Nauty.Max.Parent.key {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {p : Parent n} (h : Valid G ctx tcLevel p) : Frame.key ctx tcLevel (child ctx tcLevel p) = Loop.key ctx tcLevel p.loop p.chosen

The saved child has the chosen vertex's key in the frozen sweep.

theorem Hex.GraphIso.Nauty.Max.Loop.key_le {n : Nat} {ctx : Ctx n} {tcLevel v : Nat} {l : Loop n} (hv : (windowSet n (prepare ctx tcLevel l).snd.snd.snd.snd.lab (prepare ctx tcLevel l).snd.fst.toNat (prepare ctx tcLevel l).snd.snd.snd.fst).mem v = true) : keyLe (key ctx tcLevel l v) (bound ctx tcLevel l)

Every original target vertex is bounded by the frozen full sweep.

theorem Hex.GraphIso.Nauty.Max.Parent.key_le {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {p : Parent n} (h : Valid G ctx tcLevel p) : keyLe (Frame.key ctx tcLevel (child ctx tcLevel p)) (Loop.bound ctx tcLevel p.loop)

An actual saved child stays below the complete chosen-cell maximum.

theorem Hex.GraphIso.Nauty.Max.SweepInput.suspend {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel : Nat} {first : Bool} {level numcells tc tv1 tv index : Nat} {cell : VSet n} {st : Search n} {l : Loop n} {bs fs : List Nat} {parents : Parents n} (h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents) : Parent.Valid G ctx tcLevel { loop := l, state := st, chosen := tv, bs := bs, fs := fs }

Every selected child records the reference, shape, and target justifications already established at its actual sweep entry.

theorem Hex.GraphIso.Nauty.Max.Parents.push_frames {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {parents : Parents n} {p : Parent n} (hl : 1 ≤ p.loop.node.level) (ht : target < p.loop.node.level) (hparent : 1 < p.loop.node.level → ∃ (prev : Parent n), parents (p.loop.node.level - 1) = some prev ∧ Parent.child ctx tcLevel prev = p.loop.node) : frames ctx tcLevel (parents.push p) target = (frames ctx tcLevel parents).insert p.loop.node target

Below the child's receiving level, saving a parent preserves exactly the sweep's ancestor table, including the root frame at target zero.