structure Hex.GraphIso.Nauty.Sparse.Max.Parent (n : Nat) : Type

A suspended native parent records the actual child selection and the incumbent codes at that selection. Its mutable target may be filtered.

• node : Frame n
• first : Bool
• state : State n
• tc : Nat
• cell : VSet n
• chosen : Nat
• bs : List Nat

def Hex.GraphIso.Nauty.Sparse.Max.Parent.child {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (p : Parent n) : Frame n

Equations

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

structure Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid {n k : Nat} (G : Sparse.Colored n k) (tcLevel : Nat) (p : Parent n) : Prop

The suspended entry retains its native frame and cheap shape. A hinted target is allowed when its negative comparison already covers the parent; the positive branch retains the original target coordinate.

• node : Frame.Valid G p.node
• internal : (visit (Graph.ofGraph G.graph) p.node.level p.node.numcells p.node.entry).fst < n
• ready : Ready G p.node.level (Frame.target G.graph tcLevel p.node).numcells p.state
• effect : FrameOut G p.node.level p.node.level (Frame.target G.graph tcLevel p.node).entry p.state
• target : Generic.Target State.frame p.node.level p.tc p.cell p.state
• chosen : p.cell.mem p.chosen = true
• choice : Frame.Choice G.graph tcLevel p.node p.tc (State.key G.graph p.bs p.state)
• small : p.state.noncheaplevel ≤ p.node.level → NodeShape n p.node.level p.state.ptn

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {p : Parent n} (h : Valid G tcLevel p) : Frame.Valid G (Parent.child G.graph tcLevel p)

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.member {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {p : Parent n} (h : Valid G tcLevel p) (ht : p.tc = (Frame.target G.graph tcLevel p.node).tc) : (Frame.target G.graph tcLevel p.node).vertices.mem p.chosen = true

A selected vertex belongs to the original unfiltered window whenever the actual target coordinate agrees with the unhinted native target.

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.collapse {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {p : Parent n} (h : Valid G tcLevel p) (hc : p.state.noncheaplevel ≤ p.node.level) : Covers (Frame.key G.graph tcLevel p.node) (State.key G.graph p.bs p.state) ∨ Frame.key G.graph tcLevel p.node = Frame.key G.graph tcLevel (Parent.child G.graph tcLevel p)

A cheap parent's full key is covered already or equals the key of its actual chosen child. The two cases are the literal target-choice alternatives; no whole-search correctness is assumed.

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.child_bound {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {p : Parent n} (h : Valid G tcLevel p) : (Frame.key G.graph tcLevel (Parent.child G.graph tcLevel p)).Le (incMax (State.key G.graph p.bs p.state) (Frame.key G.graph tcLevel p.node))

Every actual selected child stays below the parent's allowed upper bound. A hinted child is bounded by its negative code prefix, even when it does not belong to the unhinted specification target.

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Sparse.Max.Parents (n : Nat) : Type

Suspended native parents are indexed by their node level.

Equations

• Hex.GraphIso.Nauty.Sparse.Max.Parents n = (Nat → Option (Hex.GraphIso.Nauty.Sparse.Max.Parent n))

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

Equations

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

def Hex.GraphIso.Nauty.Sparse.Max.Parents.frames {n : Nat} (parents : Parents n) : Frames n

Return target zero names the root entry; every later target names the frozen entry at the next level.

Equations

• parents.frames target = Option.map Hex.GraphIso.Nauty.Sparse.Max.Parent.node (parents (target + 1))

theorem Hex.GraphIso.Nauty.Sparse.Max.Parents.push_frames {n : Nat} {parents : Parents n} {p : Parent n} (hp : 1 ≤ p.node.level) : (parents.push p).frames = parents.frames.insert p.node