theorem Hex.GraphIso.Nauty.Sparse.Order.admit {n : Nat} {κ : Type} (st : SearchState n κ) : (Nauty.admit st).order = st.order

theorem Hex.GraphIso.Nauty.Sparse.Order.leaf {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.order = st.order

theorem Hex.GraphIso.Nauty.Sparse.Order.target {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (chooseTarget first g tcLevel level numcells st).snd.snd.snd.order = st.order

theorem Hex.GraphIso.Nauty.Sparse.Order.classify {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : (Sparse.classify g level numcells st).snd.order = st.order

theorem Hex.GraphIso.Nauty.Sparse.Order.cheap {n : Nat} (first : Bool) (level : Nat) (st : State n) : (cheapCheck first level st).order = st.order

theorem Hex.GraphIso.Nauty.Sparse.Order.child {n : Nat} (first : Bool) (level tc tv : Nat) (st : State n) : (Generic.Policy.child first level tc tv st).order = st.order

theorem Hex.GraphIso.Nauty.Sparse.Order.recover {n : Nat} (inf level : Nat) (st : State n) : (Generic.Policy.recover inf level st).order = st.order

theorem Hex.GraphIso.Nauty.Sparse.Order.close {n : Nat} (first : Bool) (level size index : Nat) (st : State n) : (Generic.Policy.afterSweep first level size index st).order = if first = true then st.order * index else st.order

Only closing a first-path sweep changes the accumulator.

theorem Hex.GraphIso.Nauty.Sparse.Order.prepare {n : Nat} (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (Generic.prepareFirst g tcLevel level numcells st).snd.snd.snd.snd.order = st.order

Refinement, target selection and first-code installation retain the incoming accumulator before the first child is individualized.

theorem Hex.GraphIso.Nauty.Sparse.Order.policy {n : Nat} (g : Graph n) (inf tcLevel value : Nat) : Generic.StablePolicy g inf tcLevel fun (st : State n) => st.order = value

The off-path policy preserves the actual order accumulator through every refinement, admission, pruning return and recovery.

theorem Hex.GraphIso.Nauty.Sparse.Order.node {n : Nat} (g : Graph n) (inf tcLevel fuel level numcells : Nat) (st : State n) : (Generic.node false g inf tcLevel fuel level numcells st).snd.order = st.order

theorem Hex.GraphIso.Nauty.Sparse.Order.sweep {n : Nat} (first : Bool) (g : Graph n) (inf tcLevel fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) (hpast : Generic.Past first tv1 cursor) : (Generic.sweep first g inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.order = st.order

theorem Hex.GraphIso.Nauty.Sparse.Order.first {n : Nat} (g : Graph n) (inf tcLevel fuel cfuel level numcells tc tv index : Nat) (cell : VSet n) (st : State n) (horbit : st.orbits[tv]! = tv) : (Generic.sweep true g inf tcLevel fuel (cfuel + 1) level numcells tc tv (some tv) cell index st).snd.snd.order = (Generic.node true g inf tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child true level tc tv st)).snd.order

The full first sweep retains exactly the guiding child's order accumulator, before the receiver multiplies by its own index.