def Hex.GraphIso.Aut.Orbit {n k : Nat} (G : Colored n k) (base : List (Fin n)) (u v : Fin n) : Prop

The orbit relation for the full pointwise stabilizer of a base.

Equations

• Hex.GraphIso.Aut.Orbit G base u v = ∃ (p : Hex.GraphIso.Perm n), Hex.GraphIso.IsIso G G p ∧ Hex.GraphIso.Perm.Fixes base p ∧ p.get u = v

theorem Hex.GraphIso.Aut.Orbit.refl {n k : Nat} (G : Colored n k) (base : List (Fin n)) (u : Fin n) : Orbit G base u u

theorem Hex.GraphIso.Aut.Orbit.trans {n k : Nat} {G : Colored n k} {base : List (Fin n)} {u v w : Fin n} (h : Orbit G base u v) (h' : Orbit G base v w) : Orbit G base u w

theorem Hex.GraphIso.Aut.Orbit.symm {n k : Nat} {G : Colored n k} {base : List (Fin n)} {u v : Fin n} (h : Orbit G base u v) : Orbit G base v u

def Hex.GraphIso.Aut.Carries {n k : Nat} (G : Colored n k) (base : List (Fin n)) (u v : Fin n) : Prop

Two vertices are related by a generated automorphism in the pointwise stabilizer of the given base. Only the resulting permutation must fix the base; the final generator list need not be a strong generating set.

Equations

• Hex.GraphIso.Aut.Carries G base u v = ∃ (p : Hex.GraphIso.Perm n), Hex.GraphIso.Perm.Generated (Hex.GraphIso.Aut.gens G) p ∧ Hex.GraphIso.Perm.Fixes base p ∧ p.get u = v

theorem Hex.GraphIso.Aut.Carries.refl {n k : Nat} (G : Colored n k) (base : List (Fin n)) (u : Fin n) : Carries G base u u

theorem Hex.GraphIso.Aut.Carries.trans {n k : Nat} {G : Colored n k} {base : List (Fin n)} {u v w : Fin n} (h : Carries G base u v) (h' : Carries G base v w) : Carries G base u w

theorem Hex.GraphIso.Aut.Carries.symm {n k : Nat} {G : Colored n k} {base : List (Fin n)} {u v : Fin n} (h : Carries G base u v) : Carries G base v u

theorem Hex.GraphIso.Aut.Carries.witness {n k : Nat} {G : Colored n k} {base : List (Fin n)} {u v : Fin n} (h : Carries G base u v) : ∃ (p : Perm n), Perm.Generated (gens G) p ∧ IsIso G G p ∧ Perm.Fixes base p ∧ p.get u = v

A generated carrier is in particular a genuine automorphism.

theorem Hex.GraphIso.Aut.Carries.orbit {n k : Nat} {G : Colored n k} {base : List (Fin n)} {u v : Fin n} (h : Carries G base u v) : Orbit G base u v

theorem Hex.GraphIso.Nauty.Generation.cellStab_fixes {ptn lab γ : Array Nat} {level pos : Nat} (hpos : pos < lab.size) (hcell : IsCell ptn level pos 1) (h : CellStab ptn level lab γ) : γ[lab[pos]!]! = lab[pos]!

A cell-stabilizing array fixes every vertex in a singleton cell.

theorem Hex.GraphIso.Nauty.Generation.carries_word {n k : Nat} {G : Colored n k} {base : List (Fin n)} {u v : Fin n} {w : List (Array Nat)} (htrace : ∀ (γ : Array Nat), γ ∈ w → γ ∈ Aut.trace G) (hfix : ∀ (γ : Array Nat), γ ∈ w → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) (hmap : applyWord w ↑u = ↑v) : Aut.Carries G base u v

A word in the final trace gives a generated carrier fixing the base when its letters stabilize the active frame's singleton base cells.

theorem Hex.GraphIso.Nauty.Generation.carries_fmperm {n k : Nat} {G : Colored n k} {base : List (Fin n)} {γ : Array Nat} (htrace : γ ∈ Aut.trace G) (hfix : ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) {v : Fin n} (hdrop : (fmperm γ n).snd.mem ↑v = false) : ∃ (u : Fin n), ↑u < ↑v ∧ Aut.Carries G base v u

The powers used by an explicit pruning pair fix the active base whenever its recorded generator does. No converse about the pair's fixed point bitset is needed.

theorem Hex.GraphIso.Nauty.Generation.carries_pointer {n k : Nat} {G : Colored n k} {base : List (Fin n)} {store : List (Array Nat)} {orbits : Array Nat} {v : Fin n} (hsound : OrbSound (OrbConn store n) orbits n) (htrace : ∀ (γ : Array Nat), γ ∈ store → γ ∈ Aut.trace G) (hfix : ∀ (γ : Array Nat), γ ∈ store → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) : ∃ (u : Fin n), ↑u = orbits[↑v]! ∧ ↑u ≤ ↑v ∧ Aut.Carries G base v u

A sound stored orbit pointer is a carrier in the generated stabilizer when the trace letters fix the active base.

theorem Hex.GraphIso.Nauty.Generation.PairGenerated.carries {n k : Nat} {G : Colored n k} {base : List (Fin n)} {fix mcr : VSet n} (h : PairGenerated G fix mcr) (hbase : ∀ (b : Fin n), b ∈ base → fix.mem ↑b = true) {v : Fin n} (hv : mcr.mem ↑v = false) : ∃ (u : Fin n), ↑u < ↑v ∧ Aut.Carries G base v u

Reading the ranked carrier of a pruning pair in the base stabilizer.