theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.firstParent_key {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : State.key G bs (firstParent G tcLevel f bs tv).state = State.key G bs f.entry

First preparation and its cheap check retain the incoming native key.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.firstParent_boundary {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : (firstParent G tcLevel f bs tv).state.noncheaplevel = f.entry.noncheaplevel ∨ f.level ≤ (firstParent G tcLevel f bs tv).state.noncheaplevel

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.otherParent_key {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : State.key G bs (otherParent G tcLevel f bs tv).state = State.key G bs f.entry

Off-path preparation and its cheap check retain the incoming native key.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.otherParent_boundary {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : (otherParent G tcLevel f bs tv).state.noncheaplevel = f.entry.noncheaplevel ∨ f.level ≤ (otherParent G tcLevel f bs tv).state.noncheaplevel

theorem Hex.GraphIso.Nauty.Sparse.Max.Scope.first_child {n k : Nat} {G : Sparse.Colored n k} {tcLevel tv : Nat} {f : Frame n} {bs : List Nat} {parents : Parents n} (h : Scope G tcLevel f bs f.entry parents) (hv : Frame.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) : have p := Frame.firstParent G.graph tcLevel f bs tv; Scope G tcLevel (Parent.child G.graph tcLevel p) bs (Parent.child G.graph tcLevel p).entry (parents.push p)

The ancestor invariant is established at the actual first child, including its prepared target and inherited cheap shape.

theorem Hex.GraphIso.Nauty.Sparse.Max.Scope.other_child {n k : Nat} {G : Sparse.Colored n k} {tcLevel tv : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : Scope G tcLevel f bs f.entry parents) (hv : Frame.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) : have p := Frame.otherParent G.graph tcLevel f bs tv; Scope G tcLevel (Parent.child G.graph tcLevel p) bs (Parent.child G.graph tcLevel p).entry (parents.push p)

Native off-path preparation establishes the child scope from the incoming comparison machines; all hinted-target obligations are discharged.

theorem Hex.GraphIso.Nauty.Sparse.Max.Scope.node {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : Scope G tcLevel f bs f.entry parents) (hv : Frame.Valid G f) (hi : CodeEntry G tcLevel f.level f.numcells f.entry) (hc : Comparison G.graph f.codes bs fs f.entry) (hf : n ≤ f.codes.length + fuel) : have out := (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).snd; ∃ (ds : List Nat), ReturnCodes G.graph f.codes ds fs out ∧ Scope G tcLevel f ds out parents

A complete actual off-path call preserves every suspended ancestor. Both required effects come from the executed code and boundary proofs, independently of the outstanding maximum theorem.