def Hex.GraphIso.Nauty.Sparse.Max.Parent.key {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (p : Parent n) (v : Nat) : Key n

Full child keys at the actual suspended target, retaining its native arrays before the descendant call. The target may be hinted or filtered.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.child_key {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (p : Parent n) : Frame.key G tcLevel (child G tcLevel p) = key G tcLevel p p.chosen

The executed individualization has exactly the suspended selected vertex's full key, including its actual code prefix.

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.scatter_cover {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {p : Parent n} (h : Valid G tcLevel p) {ref lab gamma : Array Nat} {best : Option (Key n)} (ha : Automorphism G gamma) (href : ref.size = n) (hfr : cellsPerm p.state.ptn p.node.level p.state.lab ref) (hl : cellsPerm p.state.ptn p.node.level p.state.lab lab) (hmap : ∀ (i : Nat), i < n → gamma[ref[i]!]! = lab[i]!) (hchosen : lab[p.tc]! = p.chosen) (hcover : Covers (key G.graph tcLevel p ref[p.tc]!) best) : Covers (Frame.key G.graph tcLevel (Parent.child G.graph tcLevel p)) best

A native automorphism scattering a covered reference labelling to the current descendant covers the suspended parent's entire chosen child. This transports all unpruned leaves, regardless of the emitter's depth.