def Hex.GraphIso.Nauty.Sparse.Automorphism {n k : Nat} (G : Sparse.Colored n k) (values : Array Nat) : Prop

Every entry of an emitted array is the forward map of a native colour-preserving automorphism, and the array has exactly the graph order.

Equations

• Hex.GraphIso.Nauty.Sparse.Automorphism G values = (values.size = n ∧ ∃ (p : Hex.Perm n), Hex.GraphIso.Sparse.IsIso G G p ∧ ∀ (v : Fin n), values[↑v]! = ↑(p.get v))

def Hex.GraphIso.Nauty.Sparse.TraceOk {n k : Nat} (G : Sparse.Colored n k) (st : State n) : Prop

Soundness of every array in the executed, unbounded generator trace.

Equations

• Hex.GraphIso.Nauty.Sparse.TraceOk G st = ∀ (values : Array Nat), values ∈ st.genTrace → Hex.GraphIso.Nauty.Sparse.Automorphism G values

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

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.congr {n k : Nat} {G : Sparse.Colored n k} {st out : State n} (h : TraceOk G st) (he : out.genTrace = st.genTrace) : TraceOk G out

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.initial {n k : Nat} (G : Sparse.Colored n k) (lab : Array Nat) (ends : List Nat) : TraceOk G (Sparse.initial (Graph.ofGraph G.graph) lab ends)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.visit {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (level numcells : Nat) : TraceOk G (Sparse.visit (Graph.ofGraph G.graph) level numcells st).snd.snd

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.record {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (level code : Nat) : TraceOk G (recordFirst level code st)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.compare {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (level code : Nat) : TraceOk G (compareCodes level code st)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.target {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (first : Bool) (tcLevel level numcells : Nat) : TraceOk G (chooseTarget first (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.snd

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.classify {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (level numcells : Nat) : TraceOk G (Sparse.classify (Graph.ofGraph G.graph) level numcells st).snd

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.terminal {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (level : Nat) : TraceOk G (firstterminal level st)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.cheap {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (first : Bool) (level : Nat) : TraceOk G (cheapCheck first level st)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.child {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (first : Bool) (level tc tv : Nat) : TraceOk G (Generic.Policy.child first level tc tv st)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.afterChild {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (level tv : Nat) : TraceOk G (afterChildFirst level tv st)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.leave {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (tv : Nat) : TraceOk G (Generic.Policy.leaveChild tv st)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.recover {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (inf level : Nat) : TraceOk G (Generic.Policy.recover inf level st)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.afterSweep {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (first : Bool) (level size index : Nat) : TraceOk G (Generic.Policy.afterSweep first level size index st)

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.leaf {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) (leaf : Leaf) (level : Nat) (ha : leaf = Generic.Leaf.autoFirst ∨ leaf = Generic.Leaf.autoCanon → Automorphism G st.workperm) : TraceOk G (leafExit leaf level st).snd

Each actual automorphism leaf action appends exactly its checked workspace; every other action preserves the trace without appending.

theorem Hex.GraphIso.Nauty.Sparse.classify_auto {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (hn : 0 < n) (h : Ready G level numcells st) (hh : CheapHistory G.graph tcLevel level level numcells st) (hs : Store G.graph st) (hc : CanonLabel G st) (hf : st.firstlab.size = n ∧ CellsReach G.toDense st.firstlab) (hw : st.workperm.size = n) : have r := classify (Graph.ofGraph G.graph) level numcells st; r.fst = Generic.Leaf.autoFirst ∨ r.fst = Generic.Leaf.autoCanon → Automorphism G r.snd.workperm

Both native automorphism verdicts supply a sound array for the emitted trace, using the frozen first history or the actual canonical row prefix.