def Hex.GraphIso.Nauty.CellStab (ptn : Array Nat) (level : Nat) (lab γ : Array Nat) : Prop

γ fixes each cell's content set: the labelling mapped through γ is cell-wise a permutation of itself.

Equations

• Hex.GraphIso.Nauty.CellStab ptn level lab γ = Hex.GraphIso.Nauty.cellsPerm ptn level lab (Array.map (fun (w : Nat) => γ[w]!) lab)

theorem Hex.GraphIso.Nauty.cellStab_range {n : Nat} {ptn lab : Array Nat} {level : Nat} (hok : LabOk lab n) : CellStab ptn level lab (Array.range n)

theorem Hex.GraphIso.Nauty.cellStab_comp {n : Nat} {ptn lab f π : Array Nat} {level : Nat} (hok : LabOk lab n) (hsp : ptn.size = n) (hs : lab.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hf : CellStab ptn level lab f) (hπ : CellStab ptn level lab π) : CellStab ptn level lab (composePerm f π n)

theorem Hex.GraphIso.Nauty.checkAutom_bound {n : Nat} {g : Array (VSet n)} {γ : Array Nat} (h : checkAutom g γ = true) (v : Nat) : v < n → γ[v]! < n

Bound extraction from a checked automorphism.

def Hex.GraphIso.Nauty.applyWord (w : List (Array Nat)) (v : Nat) : Nat

Apply a word of generators, leftmost first.

Equations

• Hex.GraphIso.Nauty.applyWord w v = List.foldl (fun (v : Nat) (γ : Array Nat) => γ[v]!) v w

def Hex.GraphIso.Nauty.wordPerm (nn : Nat) : List (Array Nat) → Array Nat

The composite permutation array carried by a word.

Equations

• Hex.GraphIso.Nauty.wordPerm nn [] = Array.range nn
• Hex.GraphIso.Nauty.wordPerm nn (γ :: w) = Hex.GraphIso.Nauty.composePerm (Hex.GraphIso.Nauty.wordPerm nn w) γ nn

theorem Hex.GraphIso.Nauty.wordPerm_spec {n : Nat} {g : Array (VSet n)} {ptn lab : Array Nat} {level : Nat} (hok : LabOk lab n) (hsp : ptn.size = n) (hs : lab.size = n) (hend : ptn[ptn.size - 1]! ≤ level) {S : List (Array Nat)} (hv : ∀ (γ : Array Nat), γ ∈ S → checkAutom g γ = true) (hstab : ∀ (γ : Array Nat), γ ∈ S → CellStab ptn level lab γ) (w : List (Array Nat)) : (∀ (γ : Array Nat), γ ∈ w → γ ∈ S) → checkAutom g (wordPerm n w) = true ∧ CellStab ptn level lab (wordPerm n w) ∧ ∀ (v : Nat), v < n → (wordPerm n w)[v]! = applyWord w v

A word of stored generators composes to a checked automorphism that still stabilizes the cells and acts as the word does.

theorem Hex.GraphIso.Nauty.foldl_invariant {α β : Type} {P : α → Prop} {step : α → β → α} (l : List β) (s : α) : P s → (∀ (a : α) (b : β), b ∈ l → P a → P (step a b)) → P (List.foldl step s l)

def Hex.GraphIso.Nauty.orbitStepSet (nn : Nat) (gens : List (Array Nat)) (s : VSet nn) : VSet nn

One round of forward generator images over a vertex set.

Equations

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

def Hex.GraphIso.Nauty.orbitClose (nn : Nat) (gens : List (Array Nat)) : Nat → VSet nn → VSet nn

Iterated forward closure of a vertex set under the store. Any fuel is sound; nn rounds saturate.

Equations

• Hex.GraphIso.Nauty.orbitClose nn gens 0 x✝ = x✝
• Hex.GraphIso.Nauty.orbitClose nn gens fuel.succ x✝ = Hex.GraphIso.Nauty.orbitClose nn gens fuel (Hex.GraphIso.Nauty.orbitStepSet nn gens x✝)

theorem Hex.GraphIso.Nauty.orbitStepSet_sound {nn : Nat} {gens : List (Array Nat)} {s : VSet nn} (x : Nat) : (orbitStepSet nn gens s).mem x = true → s.mem x = true ∨ ∃ (γ : Array Nat), γ ∈ gens ∧ ∃ (u : Nat), s.mem u = true ∧ γ[u]! = x

theorem Hex.GraphIso.Nauty.orbitClose_sound {nn : Nat} {gens : List (Array Nat)} (fuel : Nat) (s : VSet nn) (x : Nat) : (orbitClose nn gens fuel s).mem x = true → ∃ (u : Nat), ∃ (w : List (Array Nat)), s.mem u = true ∧ (∀ (γ : Array Nat), γ ∈ w → γ ∈ gens) ∧ applyWord w u = x

theorem Hex.GraphIso.Nauty.isCell_succ {n : Nat} {ptn : Array Nat} {level a len : Nat} (hvals : ∀ (q : Nat), ptn[q]! ≤ level ∨ ptn[q]! = n + 2) (hlev : level + 1 < n + 2) (hic : IsCell ptn level a len) : IsCell ptn (level + 1) a len

theorem Hex.GraphIso.Nauty.isCell_pred {n : Nat} {ptn : Array Nat} {level a len : Nat} (hvals : ∀ (q : Nat), ptn[q]! ≤ level ∨ ptn[q]! = n + 2) (hlev : level + 1 < n + 2) (hic : IsCell ptn (level + 1) a len) : IsCell ptn level a len

def Hex.GraphIso.Nauty.orbPruned (nn : Nat) (gens : List (Array Nat)) (rsLab : Array Nat) (tc o : Nat) : Bool

The fmptn-style skip: child o is dropped when its target vertex reaches an earlier sibling's under forward closure of the store. No single carrying generator is exhibited.

Equations

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

theorem Hex.GraphIso.Nauty.childKey_of_orbPruned {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {gens : List (Array Nat)} (hv : ∀ (γ : Array Nat), γ ∈ gens → checkAutom ctx.g γ = true) (tcLevel fuel level : Nat) {rsLab rsPtn : Array Nat} {tc lenT numcells o : Nat} (hstab : ∀ (γ : Array Nat), γ ∈ gens → CellStab rsPtn level rsLab γ) (hs : rsLab.size = n) (hok : LabOk rsLab n) (hsp : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hic : IsCell rsPtn level tc lenT) (hrange : tc + lenT ≤ n) (ho : o < lenT) (hlf : level + 1 + fuel ≤ n + 1) (hpr : orbPruned n gens rsLab tc o = true) : ∃ (o' : Nat), o' < o ∧ childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o' = childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o

An orbit-pruned position's key repeats an earlier sibling's: the orbit path composes to a checked, cell-stabilizing automorphism carrying one breakout n labelling to the other, and specNode_autom transports the subtree key. This is the justification of the fmptn discipline at one node.

def Hex.GraphIso.Nauty.WordConn (gens : List (Array Nat)) (u v : Nat) : Prop

Connectivity by a forward word over a generator store: some list of stored arrays, applied leftmost first, carries u to v.

Equations

• Hex.GraphIso.Nauty.WordConn gens u v = ∃ (w : List (Array Nat)), (∀ (γ : Array Nat), γ ∈ w → γ ∈ gens) ∧ Hex.GraphIso.Nauty.applyWord w u = v

theorem Hex.GraphIso.Nauty.wordConn_refl (gens : List (Array Nat)) (u : Nat) : WordConn gens u u

theorem Hex.GraphIso.Nauty.applyWord_append (w₁ w₂ : List (Array Nat)) (u : Nat) : applyWord (w₁ ++ w₂) u = applyWord w₂ (applyWord w₁ u)

theorem Hex.GraphIso.Nauty.wordConn_trans {gens : List (Array Nat)} {u v x : Nat} (h₁ : WordConn gens u v) (h₂ : WordConn gens v x) : WordConn gens u x

theorem Hex.GraphIso.Nauty.wordConn_step {gens : List (Array Nat)} {γ : Array Nat} (hγ : γ ∈ gens) (u : Nat) : WordConn gens u γ[u]!

theorem Hex.GraphIso.Nauty.wordConn_mono {gens gens' : List (Array Nat)} {u v : Nat} (hsub : ∀ (γ : Array Nat), γ ∈ gens → γ ∈ gens') (h : WordConn gens u v) : WordConn gens' u v

theorem Hex.GraphIso.Nauty.applyWord_replicate_succ (γ : Array Nat) (k u : Nat) : applyWord (List.replicate (k + 1) γ) u = applyWord (List.replicate k γ) γ[u]!

theorem Hex.GraphIso.Nauty.applyWord_replicate_lt {n : Nat} {γ : Array Nat} (hb : ∀ (v : Nat), v < n → γ[v]! < n) (k : Nat) {u : Nat} : u < n → applyWord (List.replicate k γ) u < n

theorem Hex.GraphIso.Nauty.applyWord_replicate_inj {n : Nat} {γ : Array Nat} (hb : ∀ (v : Nat), v < n → γ[v]! < n) (hinj : ∀ (a b : Nat), a < n → b < n → γ[a]! = γ[b]! → a = b) (k : Nat) {a b : Nat} : a < n → b < n → applyWord (List.replicate k γ) a = applyWord (List.replicate k γ) b → a = b

theorem Hex.GraphIso.Nauty.exists_applyWord_replicate_self {n : Nat} {γ : Array Nat} (hb : ∀ (v : Nat), v < n → γ[v]! < n) (hinj : ∀ (a b : Nat), a < n → b < n → γ[a]! = γ[b]! → a = b) {u : Nat} (hu : u < n) : ∃ (k : Nat), 0 < k ∧ applyWord (List.replicate k γ) u = u

A bounded injective array returns every vertex to itself under some positive number of forward applications.

theorem Hex.GraphIso.Nauty.wordConn_symm {n : Nat} {gens : List (Array Nat)} (hb : ∀ (γ : Array Nat), γ ∈ gens → ∀ (v : Nat), v < n → γ[v]! < n) (hinj : ∀ (γ : Array Nat), γ ∈ gens → ∀ (a b : Nat), a < n → b < n → γ[a]! = γ[b]! → a = b) (w : List (Array Nat)) {u v : Nat} : u < n → (∀ (γ : Array Nat), γ ∈ w → γ ∈ gens) → applyWord w u = v → WordConn gens v u

Symmetry of forward-word connectivity over bounded injective generators: the inverse of each letter is one of its forward powers.

def Hex.GraphIso.Nauty.OrbSound (R : Nat → Nat → Prop) (orbits : Array Nat) (n : Nat) : Prop

Soundness of an orbit-pointer array: every parent pointer descends weakly and is R-connected to its vertex. Descent keeps every pointer below n and makes the chase loops terminate within their fuel, but soundness never needs the latter fact.

Equations

• Hex.GraphIso.Nauty.OrbSound R orbits n = (orbits.size = n ∧ ∀ (v : Nat), v < n → orbits[v]! ≤ v ∧ R v orbits[v]!)

theorem Hex.GraphIso.Nauty.orbSound_ptr {n : Nat} {R : Nat → Nat → Prop} {orbits : Array Nat} (h : OrbSound R orbits n) {v : Nat} (hv : v < n) : R v orbits[v]!

The consumption form at prune sites: a consulted parent pointer is justified by R.

def Hex.GraphIso.Nauty.ptrIter (orbits : Array Nat) (v : Nat) : Nat → Nat

The k-fold iterated parent pointer, as any chase computes it.

Equations

• Hex.GraphIso.Nauty.ptrIter orbits v 0 = v
• Hex.GraphIso.Nauty.ptrIter orbits v k.succ = orbits[Hex.GraphIso.Nauty.ptrIter orbits v k]!

theorem Hex.GraphIso.Nauty.orbSound_iter {n : Nat} {R : Nat → Nat → Prop} {orbits : Array Nat} (hrefl : ∀ (v : Nat), R v v) (htrans : ∀ (a b c : Nat), R a b → R b c → R a c) (h : OrbSound R orbits n) (k : Nat) {v : Nat} : v < n → ptrIter orbits v k ≤ v ∧ R v (ptrIter orbits v k)

Any pointer chase from a sound array descends and stays R-connected.

theorem Hex.GraphIso.Nauty.orbSound_init {n : Nat} (R : Nat → Nat → Prop) (hrefl : ∀ (v : Nat), v < n → R v v) : OrbSound R (Array.ofFn fun (i : Fin n) => ↑i) n

theorem Hex.GraphIso.Nauty.orbSound_set {n : Nat} {R : Nat → Nat → Prop} {orbits : Array Nat} (h : OrbSound R orbits n) {p q : Nat} (hq : q < n) (hpq : p ≤ q) (hR : R q p) : OrbSound R (orbits.set! q p) n

theorem Hex.GraphIso.Nauty.orbSound_mono {n : Nat} {R R' : Nat → Nat → Prop} {orbits : Array Nat} (himp : ∀ (a b : Nat), R a b → R' a b) (h : OrbSound R orbits n) : OrbSound R' orbits n

theorem Hex.GraphIso.Nauty.orbjoin_orbSound {n : Nat} {R : Nat → Nat → Prop} (hsymm : ∀ (a b : Nat), R a b → R b a) (htrans : ∀ (a b c : Nat), R a b → R b c → R a c) {orbits map : Array Nat} (h : OrbSound R orbits n) (hmap : ∀ (i : Nat), i < n → map[i]! < n ∧ R i map[i]!) : OrbSound R (orbjoin orbits map n).fst n

def Hex.GraphIso.Nauty.OrbConn (gens : List (Array Nat)) (n a b : Nat) : Prop

The connectivity relation the search's orbit array maintains: both vertices in range, joined by a forward word over the store.

Equations

• Hex.GraphIso.Nauty.OrbConn gens n a b = (a < n ∧ b < n ∧ Hex.GraphIso.Nauty.WordConn gens a b)

theorem Hex.GraphIso.Nauty.orbConn_symm {n : Nat} {gens : List (Array Nat)} (hb : ∀ (γ : Array Nat), γ ∈ gens → ∀ (v : Nat), v < n → γ[v]! < n) (hinj : ∀ (γ : Array Nat), γ ∈ gens → ∀ (a b : Nat), a < n → b < n → γ[a]! = γ[b]! → a = b) (a b : Nat) : OrbConn gens n a b → OrbConn gens n b a

theorem Hex.GraphIso.Nauty.orbConn_trans {n : Nat} (gens : List (Array Nat)) (a b c : Nat) : OrbConn gens n a b → OrbConn gens n b c → OrbConn gens n a c

theorem Hex.GraphIso.Nauty.orbConn_mono {n : Nat} {gens gens' : List (Array Nat)} (hsub : ∀ (γ : Array Nat), γ ∈ gens → γ ∈ gens') (a b : Nat) : OrbConn gens n a b → OrbConn gens' n a b

theorem Hex.GraphIso.Nauty.checkAutom_inj {n : Nat} {g : Array (VSet n)} {γ : Array Nat} (h : checkAutom g γ = true) (a b : Nat) : a < n → b < n → γ[a]! = γ[b]! → a = b

Injectivity on [0, n) extracted from a checked automorphism's permutation conjunct.

theorem Hex.GraphIso.Nauty.orbSound_orbConn_init {n : Nat} (gens : List (Array Nat)) : OrbSound (OrbConn gens n) (Array.ofFn fun (i : Fin n) => ↑i) n

The identity orbit array is sound for any store.

theorem Hex.GraphIso.Nauty.orbjoin_orbConn {n : Nat} {gens : List (Array Nat)} (hb : ∀ (γ : Array Nat), γ ∈ gens → ∀ (v : Nat), v < n → γ[v]! < n) (hinj : ∀ (γ : Array Nat), γ ∈ gens → ∀ (a b : Nat), a < n → b < n → γ[a]! = γ[b]! → a = b) {orbits γ : Array Nat} (hγ : γ ∈ gens) (h : OrbSound (OrbConn gens n) orbits n) : OrbSound (OrbConn gens n) (orbjoin orbits γ n).fst n

orbjoin with a stored generator keeps every pointer justified: the run-level per-admission step. hγ names the workperm's membership in the store the pointers are read against, so joining with a newly admitted generator instantiates gens to the store after admission (earlier pointers transport by orbSound_orbConn_mono).

theorem Hex.GraphIso.Nauty.orbSound_orbConn_mono {n : Nat} {gens gens' : List (Array Nat)} (hsub : ∀ (γ : Array Nat), γ ∈ gens → γ ∈ gens') {orbits : Array Nat} (h : OrbSound (OrbConn gens n) orbits n) : OrbSound (OrbConn gens' n) orbits n

Store growth transports pointer soundness.

theorem Hex.GraphIso.Nauty.orbConn_of_ptr {n : Nat} {gens : List (Array Nat)} {orbits : Array Nat} (h : OrbSound (OrbConn gens n) orbits n) {v : Nat} (hv : v < n) : orbits[v]! < n ∧ WordConn gens v orbits[v]!

The consumption form at the transcription's prune sites: a consulted parent pointer is a forward word of stored generators, with both endpoints in range.