def Hex.GraphIso.Nauty.Generation.PairGenerated {n k : Nat} (G : Colored n k) (fix mcr : VSet n) : Prop

Each vertex omitted by a pruning pair has a strictly smaller image under a generated automorphism fixing the pair's fixed points.

Equations

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

theorem Hex.GraphIso.Nauty.Generation.pair_explicit {n k : Nat} {G : Colored n k} {γ : Array Nat} (hγ : γ ∈ Aut.trace G) : PairGenerated G (fmperm γ n).fst (fmperm γ n).snd

The carriers of an explicit pair are powers of its recorded generator, so they lie in the subgroup generated by the final trace.

theorem Hex.GraphIso.Nauty.Generation.pair_implicit {n k : Nat} {G : Colored n k} {fix mcr : VSet n} {base : List (Fin n)} (hpair : PairOk (rowsOf G) (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 fix mcr) (hbase : ∀ (v : Fin n), v ∈ base → fix.mem ↑v = true) (hnext : ∀ (p : Perm n), IsIso G G p → Perm.Fixes base p → Perm.Generated (Aut.gens G) p) : PairGenerated G fix mcr

An implicit pair whose fixed points include the next stabilizer base has generated carriers by the downward stabilizer-chain hypothesis.

theorem Hex.GraphIso.Nauty.Generation.pruned_generated {n k : Nat} {G : Colored n k} {base : List (Fin n)} {W R : VSet n} (hstable : ∀ (p : Perm n), IsIso G G p → Perm.Fixes base p → ∀ (v : Fin n), W.mem ↑v = true → W.mem ↑(p.get v) = true) (hdrop : ∀ (v : Fin n), W.mem ↑v = true → R.mem ↑v = false → ∃ (p : Perm n), Perm.Generated (Aut.gens G) p ∧ IsIso G G p ∧ Perm.Fixes base p ∧ ↑(p.get v) < ↑v) (v : Fin n) : W.mem ↑v = true → ∃ (p : Perm n), Perm.Generated (Aut.gens G) p ∧ IsIso G G p ∧ Perm.Fixes base p ∧ W.mem ↑(p.get v) = true ∧ R.mem ↑(p.get v) = true

Repeated removal by generated carriers reaches a survivor. The strictly decreasing vertex index is the same termination argument used by the executable pruning proof, with subgroup membership retained.

theorem Hex.GraphIso.Nauty.Generation.shortprune_generated {n k : Nat} {G : Colored n k} {base : List (Fin n)} {W : VSet n} {st : SearchSt n} (hstable : ∀ (p : Perm n), IsIso G G p → Perm.Fixes base p → ∀ (v : Fin n), W.mem ↑v = true → W.mem ↑(p.get v) = true) (hlast : ∀ (fix mcr : VSet n), st.autos.back? = some (fix, mcr) → PairGenerated G fix mcr ∧ ∀ (v : Fin n), v ∈ base → fix.mem ↑v = true) (v : Fin n) : W.mem ↑v = true → ∃ (p : Perm n), Perm.Generated (Aut.gens G) p ∧ IsIso G G p ∧ Perm.Fixes base p ∧ W.mem ↑(p.get v) = true ∧ (shortprune W st).mem ↑(p.get v) = true

A short-prune filter retains a representative of every orbit of the current point stabilizer when its last pair has generated carriers.