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

A carrier is generated by the supplied final list and fixes the active base. The list is independent of either search implementation.

Equations

• Hex.GraphIso.Nauty.Generation.Carries G gs base u v = ∃ (p : Hex.Perm n), Hex.GraphIso.Perm.Generated gs p ∧ Hex.GraphIso.IsIso G G p ∧ Hex.GraphIso.Perm.Fixes base p ∧ p.get u = v

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

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

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

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

theorem Hex.GraphIso.Nauty.Generation.Carries.mono {n k : Nat} {G : Colored n k} {gs : List (Perm n)} {base : List (Fin n)} {u v : Fin n} {more : List (Perm n)} (h : Carries G gs base u v) (hsub : ∀ (p : Perm n), p ∈ gs → p ∈ more) : Carries G more base u v

Retaining the emitted generators retains their carrier words.

def Hex.GraphIso.Nauty.Generation.Realizes {n k : Nat} (G : Colored n k) (gs : List (Perm n)) (store : List (Array Nat)) : Prop

Every recorded array is represented in the supplied generated group, with its exact pointwise action and colour preservation.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Generation.Realizes.mono {n k : Nat} {G : Colored n k} {gs : List (Perm n)} {before after : List (Array Nat)} (h : Realizes G gs after) (hsub : ∀ (γ : Array Nat), γ ∈ before → γ ∈ after) : Realizes G gs before

Restricting a containing trace preserves all admission witnesses.

theorem Hex.GraphIso.Nauty.Generation.realized_trace {n k : Nat} {G : Colored n k} {st : Search n} (h : RunInv G { g := rowsOf G } st) : Realizes G (List.filterMap (autom? G) st.genTrace.toList) st.genTrace.toList

A checked search output realizes its own filtered trace. This uses only array admission and its initial-colour invariant.

theorem Hex.GraphIso.Nauty.Generation.Realizes.word {n k : Nat} {G : Colored n k} {gs : List (Perm n)} (w : List (Array Nat)) : Realizes G gs w → ∃ (p : Perm n), Perm.Generated gs p ∧ IsIso G G p ∧ ∀ (v : Fin n), ↑(p.get v) = applyWord w ↑v

A word in the retained trace acts as a generated colour-preserving permutation, including repeated and redundant generators.

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

Recorded words fixing the active base supply generated carriers.

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

An orbit pointer is a generated carrier when its actual trace fixes the active base and is included in the final containing trace.

theorem Hex.GraphIso.Nauty.Generation.carries_label {n k : Nat} {G : Colored n k} {gs : List (Perm n)} {base : List (Fin n)} {ctx : Ctx n} {ref cur : Array Nat} {store : Array (Array Nat)} {pos : Nat} {u v : Fin n} (h : LabelCarrier ctx ref cur store) (htrace : Realizes G gs store.toList) (hfix : ∀ (γ : Array Nat), γ ∈ store → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) (hpos : pos < n) (href : ref[pos]! = ↑u) (hcur : cur[pos]! = ↑v) : Carries G gs base u v

A returned scatter supplies the generated carrier between its reference vertex and the chosen child vertex.