def Hex.GraphIso.Nauty.OrbitsOk {n : Nat} (st : Search n) : Prop

Every orbit pointer descends and is connected by a word of recorded generators.

Equations

• Hex.GraphIso.Nauty.OrbitsOk st = Hex.GraphIso.Nauty.OrbSound (Hex.GraphIso.Nauty.OrbConn st.genTrace.toList n) st.orbits n

theorem Hex.GraphIso.Nauty.OrbitsOk.congr {n : Nat} {st out : Search n} (h : OrbitsOk st) (ht : out.genTrace = st.genTrace) (ho : out.orbits = st.orbits) : OrbitsOk out

Preserving the generator trace and pointers preserves their relation.

theorem Hex.GraphIso.Nauty.pushAuto_orbits {n : Nat} {κ : Type} (st : SearchState n κ) (pair : VSet n × VSet n) : (pushAuto st pair).orbits = st.orbits

Workspace replacement changes no orbit pointer.

theorem Hex.GraphIso.Nauty.admit_orbits {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).orbits = (orbjoin st.orbits st.workperm n).fst

Admission joins the existing pointers with the scratch permutation.

theorem Hex.GraphIso.Nauty.OrbitsOk.admit {n : Nat} {ctx : Ctx n} {st : Search n} (h : OrbitsOk st) (ht : TraceOk ctx st) (hwork : checkAutom ctx.g st.workperm = true) : OrbitsOk (Nauty.admit st)

Joining a checked admission preserves connectivity in the enlarged trace.

theorem Hex.GraphIso.Nauty.OrbitsOk.prune {n : Nat} {st : Search n} (h : OrbitsOk st) (level : Nat) : OrbitsOk (pruneReturn level st).snd

The shared prune tail retains the generator trace and its orbit relation.

theorem Hex.GraphIso.Nauty.pruneReturn_orbits {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : (pruneReturn level st).snd.orbits = st.orbits

The shared prune tail changes no orbit pointer.

theorem Hex.GraphIso.Nauty.leafExit_orbits {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.orbits = match leaf with | Generic.Leaf.autoFirst => (orbjoin st.orbits st.workperm n).fst | Generic.Leaf.autoCanon => (orbjoin st.orbits st.workperm n).fst | x => st.orbits

Only the two automorphism verdicts join new orbit pointers.

theorem Hex.GraphIso.Nauty.OrbitsOk.leaf {n : Nat} {ctx : Ctx n} {st : Search n} (h : OrbitsOk st) (ht : TraceOk ctx st) (leaf : Leaf) (level : Nat) (hc : leaf = Generic.Leaf.autoFirst ∨ leaf = Generic.Leaf.autoCanon → checkAutom ctx.g st.workperm = true) : OrbitsOk (leafExit leaf level st).snd

Every leaf action preserves pointer soundness once its admissions are checked.

theorem Hex.GraphIso.Nauty.classify_orbits {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : (classify ctx level numcells st).snd.orbits = st.orbits

Classification changes no orbit pointer, including when it fills the scratch array.

theorem Hex.GraphIso.Nauty.initial_orbits (n : Nat) (lab0 : Array Nat) (cellEnds : List Nat) : OrbitsOk (initial n lab0 cellEnds)

Identity pointers are connected in the empty initial trace.