theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.firstParent_refs
{n : Nat}
(G : SparseGraph n)
(tcLevel : Nat)
(f : Frame n)
(bs : List Nat)
(tv : Nat)
:
Actual first preparation retains both reference labels and their ancestor counters through refinement, recording, target selection and the cheap check.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.otherParent_refs
{n : Nat}
(G : SparseGraph n)
(tcLevel : Nat)
(f : Frame n)
(bs : List Nat)
(tv : Nat)
:
The actual off-path preparation retains the same reference fields, including the comparison and hinted-target branches.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Guides.first_prepare
{n : Nat}
{G : SparseGraph n}
{tcLevel : Nat}
{f : Frame n}
{parents : Parents n}
(h : Guides G tcLevel f.entry parents)
(bs : List Nat)
(tv : Nat)
:
Guides G tcLevel (Frame.firstParent G tcLevel f bs tv).state parents
theorem
Hex.GraphIso.Nauty.Sparse.Max.Guides.other_prepare
{n : Nat}
{G : SparseGraph n}
{tcLevel : Nat}
{f : Frame n}
{parents : Parents n}
(h : Guides G tcLevel f.entry parents)
(bs : List Nat)
(tv : Nat)
:
Guides G tcLevel (Frame.otherParent G tcLevel f bs tv).state parents
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.firstParent_guided
{n : Nat}
{G : SparseGraph n}
{tcLevel : Nat}
{f : Frame n}
(hf : f.entry.gcaFirst < f.level)
(hc : f.entry.gcaCanon < f.level)
(bs : List Nat)
(tv : Nat)
:
Parent.Guided G tcLevel (firstParent G tcLevel f bs tv)
A newly prepared sweep has no reference pointing to an unvisited child of its own level. Earlier covered references remain in the scope.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.otherParent_guided
{n : Nat}
{G : SparseGraph n}
{tcLevel : Nat}
{f : Frame n}
(hf : f.entry.gcaFirst < f.level)
(hc : f.entry.gcaCanon < f.level)
(bs : List Nat)
(tv : Nat)
:
Parent.Guided G tcLevel (otherParent G tcLevel f bs tv)
theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.firstBack_counters
{n : Nat}
{G : SparseGraph n}
{tcLevel fuel last : Nat}
{p : Parent n}
{leaf : State n}
(path :
have ch := child G tcLevel p;
Generic.FirstPath (Graph.ofGraph G) tcLevel fuel ch.level ch.numcells ch.entry last leaf)
:
First-child bookkeeping and recovery set both ancestors to the receiving parent. The canonical lower bound comes from the literal first-path call, including all of its later siblings.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.back_counters
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel : Nat}
{p : Parent n}
(h : Valid G tcLevel p)
(hf : 0 < p.state.gcaFirst)
(hl : p.state.gcaFirst ≤ p.node.level)
(ho : p.state.gcaFirst ≤ p.state.gcaCanon)
:
Off-path child return preserves positivity and counter order, and native recovery supplies the upper bound for the next child entry.