def Hex.GraphIso.Nauty.Sparse.Max.Frame.firstParent {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : Parent n

The parent suspended by an actual first-child call.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.Max.Frame.otherParent {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : Parent n

The parent suspended by an actual off-path child call.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.first_parent {n k : Nat} {G : Sparse.Colored n k} {tcLevel tv : Nat} {f : Frame n} (h : Valid G f) (hs : FirstShape G.graph f.level f.numcells f.entry) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (hm : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.mem tv = true) (bs : List Nat) : Parent.Valid G tcLevel (firstParent G.graph tcLevel f bs tv)

Native first preparation and its inherited cheap shape establish every suspended-parent field before descent.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.other_parent {n k : Nat} {G : Sparse.Colored n k} {tcLevel tv : Nat} {f : Frame n} {bs fs : List Nat} (h : Valid G f) (hc : Comparison G.graph f.codes bs fs f.entry) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (hm : (prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.snd.fst.mem tv = true) : Parent.Valid G tcLevel (otherParent G.graph tcLevel f bs tv)

Off-path preparation proves the complete parent invariant directly from its native comparison and guard, including the hinted-target branch.