theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.order_leaf
{n : Nat}
{G : SparseGraph n}
{tcLevel fuel : Nat}
{f : Frame n}
(hd : (Generic.prepareFirst (Graph.ofGraph G) tcLevel f.level f.numcells f.entry).fst = n)
:
A first discrete visit retains the incoming accumulator.
theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstInput.order_step
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel tv last : Nat}
{f : Frame n}
{leaf : State n}
{parents : Parents n}
{base : List (Fin n)}
[DecidableRel (Aut.Orbit G.toDense base)]
(h : FirstInput G tcLevel f parents)
(hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n)
(htv :
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv)
(horbit :
(cheapCheck true f.level
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells
f.entry).snd.snd.snd.snd).orbits[tv]! = tv)
(path :
have p := Frame.firstParent G.graph tcLevel f [] tv;
have ch := Parent.child G.graph tcLevel p;
Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel ch.level ch.numcells ch.entry last leaf)
(hf : n ≤ f.level + fuel)
(hbase : ∀ (b : Fin n), f.entry.fixedpts.mem ↑b = true ↔ b ∈ base)
(hreplay : OrbitReplay f.entry)
:
have guide := ⟨tv, ⋯⟩;
have p := Frame.firstParent G.graph tcLevel f [] tv;
have ch := Parent.child G.graph tcLevel p;
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel (fuel + 1) f.level f.numcells f.entry).snd.order = (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd.order * List.countP (fun (v : Fin n) => decide (Aut.Orbit G.toDense base guide v)) (List.finRange n)
The executed first node multiplies the guiding child's accumulator by the exact orbit size in the true point stabilizer. All sibling calls preserve the former, and the literal sweep counter supplies the latter.