theorem Hex.GraphIso.Nauty.Sparse.Automorphism.bound {n k : Nat} {G : Sparse.Colored n k} {values : Array Nat} (h : Automorphism G values) (v : Nat) (hv : v < n) : values[v]! < n

An emitted automorphism array takes in-range vertices to in-range vertices.

theorem Hex.GraphIso.Nauty.Sparse.Automorphism.inj {n k : Nat} {G : Sparse.Colored n k} {values : Array Nat} (h : Automorphism G values) (a b : Nat) (ha : a < n) (hb : b < n) (he : values[a]! = values[b]!) : a = b

An emitted automorphism array is injective on the graph's vertices.

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

Pointer bookkeeping relative to the literal generator trace. The conditional form lets a completed trace justify its earlier joins; the initialized search separately proves the condition unconditionally.

Equations

• Hex.GraphIso.Nauty.Sparse.OrbitTrace G st = (Hex.GraphIso.Nauty.Sparse.TraceOk G st → Hex.GraphIso.Nauty.OrbSound (Hex.GraphIso.Nauty.OrbConn st.genTrace.toList n) st.orbits n)

theorem Hex.GraphIso.Nauty.Sparse.OrbitTrace.congr {n k : Nat} {G : Sparse.Colored n k} {st out : State n} (h : OrbitTrace G st) (ht : out.genTrace = st.genTrace) (ho : out.orbits = st.orbits) : OrbitTrace G out

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

theorem Hex.GraphIso.Nauty.Sparse.OrbitTrace.admit {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : OrbitTrace G st) : OrbitTrace G (Nauty.admit st)

An admission uses the new trace's permutation facts for the actual orbjoin; the old pointer witnesses transport along literal trace growth.

theorem Hex.GraphIso.Nauty.Sparse.OrbitTrace.leaf {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : OrbitTrace G st) (leaf : Leaf) (level : Nat) : OrbitTrace G (leafExit leaf level st).snd

Both automorphism exits join with their appended array. Other exits retain the pointer relation without requiring any classification premise.

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

Native classification leaves the joined pointers unchanged.

theorem Hex.GraphIso.Nauty.Sparse.orbitPolicy {n k : Nat} (G : Sparse.Colored n k) (inf tcLevel : Nat) : Generic.Preserve (Graph.ofGraph G.graph) inf tcLevel (OrbitTrace G)

Every actual policy operation preserves the trace-relative relation, including cache invalidation, first descent and the order accumulator.

theorem Hex.GraphIso.Nauty.Sparse.node_orbitTrace {n k : Nat} (G : Sparse.Colored n k) (first : Bool) (inf tcLevel fuel level numcells : Nat) (st : State n) (h : OrbitTrace G st) : OrbitTrace G (Generic.node first (Graph.ofGraph G.graph) inf tcLevel fuel level numcells st).snd

The conditional bookkeeping invariant holds for every executed call, without any input validity or termination assumptions.

theorem Hex.GraphIso.Nauty.Sparse.runColored_orbits {n k : Nat} (G : Sparse.Colored n k) : OrbSound (OrbConn (runColored G).genTrace.toList n) (runColored G).orbits n

Every final pointer descends and is connected by a word in the emitted trace. Generator validity is discharged by the initialized search theorem.

theorem Hex.GraphIso.Nauty.Sparse.orbit_word {n k : Nat} (G : Sparse.Colored n k) (v : Fin n) : (runColored G).orbits[↑v]! < n ∧ WordConn (runColored G).genTrace.toList (↑v) (runColored G).orbits[↑v]!

Each pointer consumed by the orbit filter has an in-range endpoint and an explicit forward word over the search's own emitted arrays.

theorem Hex.GraphIso.Nauty.Sparse.word_iso {n k : Nat} (G : Sparse.Colored n k) (w : List (Array Nat)) : (∀ (values : Array Nat), values ∈ w → Automorphism G values) → ∃ (p : Perm n), Sparse.IsIso G G p ∧ ∀ (v : Fin n), ↑(p.get v) = applyWord w ↑v

A forward word of native automorphism arrays acts as a native colour-preserving permutation, at every vertex simultaneously.

theorem Hex.GraphIso.Nauty.Sparse.orbit_iso {n k : Nat} (G : Sparse.Colored n k) (v : Fin n) : ∃ (p : Perm n), Sparse.IsIso G G p ∧ ↑(p.get v) = (runColored G).orbits[↑v]!

Every final orbit pointer is the image of its vertex under an actual colour-preserving automorphism. No orbit or generator completeness is assumed.