theorem Hex.GraphIso.Nauty.Sparse.Automorphism.array {n k : Nat} {G : Sparse.Colored n k} {values : Array Nat} (h : Automorphism G values) : ∃ (p : Perm n), Sparse.IsIso G G p ∧ values = renamingArray (renamingOf p)

The literal emitted array is the shared finite renaming array for its native permutation. This is a proof identity, with no executed conversion.

theorem Hex.GraphIso.Nauty.Sparse.Automorphism.checked {n k : Nat} {G : Sparse.Colored n k} {values : Array Nat} (h : Automorphism G values) : checkAutom (Graph.context G.graph).g values = true

Native automorphism soundness supplies the shared row-checker contract used in the pruning-pair mathematics.

theorem Hex.GraphIso.Nauty.Sparse.Automorphism.colors {n k : Nat} {G : Sparse.Colored n k} {values : Array Nat} (h : Automorphism G values) (hn : 0 < n) : ColorStab G.toDense values

Native colour preservation gives stabilization of the literal initial ordered colour cells.

@[reducible, inline]

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

Every retained pruning pair has checked, colour-preserving realizers at the root partition. The bounded workspace may overwrite its last slot.

Equations

• Hex.GraphIso.Nauty.Sparse.PairsOk G st = Hex.GraphIso.Nauty.PairsOk G.toDense (Hex.GraphIso.Nauty.Sparse.Graph.context G.graph) st.frame

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

theorem Hex.GraphIso.Nauty.Sparse.PairsOk.push {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : PairsOk G st) {pair : VSet n × VSet n} (hp : PairOk (Graph.context G.graph).g (initPtn n (n + 2) (Nauty.initialPartition G.toDense).snd) (Nauty.initialPartition G.toDense).fst 1 pair.fst pair.snd) : PairsOk G (pushAuto st pair)

theorem Hex.GraphIso.Nauty.Sparse.PairsOk.admit {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : PairsOk G st) (hn : 0 < n) (ha : Automorphism G st.workperm) : PairsOk G (Nauty.admit st)

Both append and overwrite admission retain valid explicit pairs.

theorem Hex.GraphIso.Nauty.Sparse.PairsOk.prune {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : PairsOk G st) {level : Nat} (hb : CheapBoundary G level st) (hl : st.noncheaplevel ≤ level) : PairsOk G (pruneReturn level st).snd

theorem Hex.GraphIso.Nauty.Sparse.PairsOk.leaf {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : PairsOk G st) (hn : 0 < n) (leaf : Leaf) (level : Nat) (hb : CheapBoundary G level st) (hl : st.noncheaplevel ≤ level) (ha : leaf = Generic.Leaf.autoFirst ∨ leaf = Generic.Leaf.autoCanon → Automorphism G st.workperm) : PairsOk G (leafExit leaf level st).snd

Every shared leaf action preserves the native workspace once its explicit automorphism or saved implicit boundary is justified.

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

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

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

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

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

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

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

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

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

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

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

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

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

The native initialized pruning workspace is empty.