def Hex.GraphIso.Nauty.Sparse.Max.Frame.emit {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) : Exit × State n

The exact off-path preparation, classification and native leaf exit.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.emit_step {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {f : Frame n} (next : Generic.SweepFn (State n) n) (h : (emit G tcLevel f).fst ≠ Generic.Exit.done) : Generic.nodeStep (Graph.ofGraph G) tcLevel next false f.level f.numcells f.entry = emit G tcLevel f

A terminal emission is the actual native node step; it invokes no sibling continuation.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.sweep_step {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {f : Frame n} (next : Generic.SweepFn (State n) n) (h : (emit G tcLevel f).fst = Generic.Exit.done) : Generic.nodeStep (Graph.ofGraph G) tcLevel next false f.level f.numcells f.entry = have p := prepareOther (Graph.ofGraph G) tcLevel f.level f.numcells f.entry; have s := next false f.level p.fst p.snd.snd.fst.toNat ((p.snd.snd.snd.fst.nextElem none).getD 0) (p.snd.snd.snd.fst.nextElem none) p.snd.snd.snd.fst 0 (cheapCheck false f.level (emit G tcLevel f).snd); match s.fst with | Generic.Exit.done => (Generic.Exit.unwind (f.level - 1) false, Generic.Policy.afterSweep false f.level p.snd.snd.snd.snd.fst s.snd.fst s.snd.snd) | x => (s.fst, s.snd.snd)

When the native dispatch continues, its remaining computation is exactly the target sweep followed by the native completion bookkeeping.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.leaf_key {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {label : Label n} (h : Valid G f) : have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry; p.fst = n → Label.ofArray? n p.snd.snd.snd.snd.snd.lab = some label → key G.graph tcLevel f = { codes := f.codes ++ [p.snd.fst] ++ [codeSentinel], graph := G.graph.relabel label.perm }

A discrete prepared native label gives the whole frozen node key, including its ancestor codes and terminal sentinel.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.leaf_bound {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs fs : List Nat} (h : Valid G f) (hi : CodeEntry G tcLevel f.level f.numcells f.entry) (hc : Comparison G.graph f.codes bs fs f.entry) (hd : (prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).fst = n) : ∃ (bs' : List Nat), ReturnCodes G.graph f.codes bs' fs (emit G.graph tcLevel f).snd ∧ Bounded (key G.graph tcLevel f) (State.key G.graph bs f.entry) (State.best G.graph (emit G.graph tcLevel f).snd) ∧ Covers (key G.graph tcLevel f) (State.best G.graph (emit G.graph tcLevel f).snd)

Every actual discrete classifier, including both automorphism branches, returns the exact permitted maximum for the complete frozen node.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.prune_bound {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs fs : List Nat} (h : Valid G f) (hc : Comparison G.graph f.codes bs fs f.entry) : have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry; p.fst ≠ n → (classify (Graph.ofGraph G.graph) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.bad → ReturnCodes G.graph f.codes bs fs (emit G.graph tcLevel f).snd ∧ Bounded (key G.graph tcLevel f) (State.key G.graph bs f.entry) (State.best G.graph (emit G.graph tcLevel f).snd) ∧ Covers (key G.graph tcLevel f) (State.best G.graph (emit G.graph tcLevel f).snd)

Nonterminal native rejection covers the complete node while retaining the incoming incumbent. Its negative code verdict is derived from the actual classifier, including the saved first-reference admission test.