theorem Hex.GraphIso.Nauty.orbitStepSet_grows {nn : Nat} {gens : List (Array Nat)} {s : VSet nn} {x : Nat} (hx : s.mem x = true) : (orbitStepSet nn gens s).mem x = true

One closure round only adds members.

theorem Hex.GraphIso.Nauty.orbitStepSet_step {nn : Nat} {gens : List (Array Nat)} {s : VSet nn} {u : Nat} {γ : Array Nat} (hγ : γ ∈ gens) (hu : u < nn) (hγu : γ[u]! < nn) (hs : s.mem u = true) : (orbitStepSet nn gens s).mem γ[u]! = true

One closure round applies every generator to every member.

theorem Hex.GraphIso.Nauty.orbitClose_grows {nn : Nat} {gens : List (Array Nat)} (fuel : Nat) (s : VSet nn) (x : Nat) : s.mem x = true → (orbitClose nn gens fuel s).mem x = true

The closure only adds members.

theorem Hex.GraphIso.Nauty.orbitClose_succ {nn : Nat} {gens : List (Array Nat)} (fuel : Nat) (s : VSet nn) : orbitClose nn gens (fuel + 1) s = orbitStepSet nn gens (orbitClose nn gens fuel s)

Rounds peel off the far end as well as the near end.

theorem Hex.GraphIso.Nauty.orbitClose_mono_fuel {nn : Nat} {gens : List (Array Nat)} {f f' : Nat} (hle : f ≤ f') {s : VSet nn} {x : Nat} : (orbitClose nn gens f s).mem x = true → (orbitClose nn gens f' s).mem x = true

More fuel never loses a member.

theorem Hex.GraphIso.Nauty.orbitClose_applyWord {nn : Nat} {gens : List (Array Nat)} (hb : ∀ (γ : Array Nat), γ ∈ gens → ∀ (v : Nat), v < nn → γ[v]! < nn) (w : List (Array Nat)) : (∀ (γ : Array Nat), γ ∈ w → γ ∈ gens) → ∀ (s : VSet nn) (u : Nat), s.mem u = true → u < nn → (orbitClose nn gens w.length s).mem (applyWord w u) = true

A word of length w.length is absorbed in w.length rounds.

theorem Hex.GraphIso.Nauty.orbitStepSet_orbitClose_nn {nn : Nat} {gens : List (Array Nat)} {s : VSet nn} : orbitStepSet nn gens (orbitClose nn gens nn s) = orbitClose nn gens nn s

The closure saturates within nn rounds. After nn rounds a further round adds nothing.

theorem Hex.GraphIso.Nauty.orbitClose_of_wordConn {nn : Nat} {gens : List (Array Nat)} (hb : ∀ (γ : Array Nat), γ ∈ gens → ∀ (v : Nat), v < nn → γ[v]! < nn) {v u : Nat} (hv : v < nn) (h : WordConn gens v u) : (orbitClose nn gens nn (VSet.empty.insert v)).mem u = true

The orbit closure is complete. Anything a forward word reaches from v is in the closure of {v} at fuel nn. This is the converse of orbitClose_sound, and the direction the domination step needs.

theorem Hex.GraphIso.Nauty.orbPruned_of_wordConn {nn : Nat} {gens : List (Array Nat)} (hb : ∀ (γ : Array Nat), γ ∈ gens → ∀ (v : Nat), v < nn → γ[v]! < nn) {rsLab : Array Nat} {tc o o' : Nat} (ho' : o' < o) (hv : rsLab[tc + o]! < nn) (hconn : WordConn gens rsLab[tc + o]! rsLab[tc + o']!) : orbPruned nn gens rsLab tc o = true

The transcription's orbit test implies the model's prune. An earlier sibling word-connected to this one makes orbPruned true, so childKey_of_orbPruned applies and the dropped child repeats a key the loop already folded in.

theorem Hex.GraphIso.Nauty.childKey_of_wordConn {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 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) (ho' : o' < lenT) (hlf : level + 1 + fuel ≤ n + 1) (hconn : WordConn gens rsLab[tc + o']! rsLab[tc + o]!) : childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o = childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o'

Word-connected members of a target cell have equal child keys. The word composes to a single checked, cell-stabilizing automorphism carrying one member onto the other, and childKey_of_carried transports the subtree key. No ordering of the two offsets is involved.

theorem Hex.GraphIso.Nauty.childKey_of_wordConn' {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 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) (ho' : o' < lenT) (hlf : level + 1 + fuel ≤ n + 1) (hconn : WordConn gens rsLab[tc + o]! rsLab[tc + o']!) : childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o = childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o'

The same, with the connection in the other direction. Forward words suffice because a checked automorphism's inverse is one of its own forward powers, which is what wordConn_symm records.

theorem Hex.GraphIso.Nauty.childKey_of_orbitPtr {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {gens : List (Array Nat)} {orbits : Array Nat} (hv : ∀ (γ : Array Nat), γ ∈ gens → checkAutom ctx.g γ = true) (tcLevel fuel level : Nat) {rsLab rsPtn : Array Nat} {tc lenT numcells o 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) (ho' : o' < lenT) (hlf : level + 1 + fuel ≤ n + 1) (hsound : OrbSound (OrbConn gens n) orbits n) (hptr : orbits[rsLab[tc + o]!]! = rsLab[tc + o']!) : childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o = childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o'

A skipped child repeats the key of its orbit pointer's target. This is the domination fact for one step of the transcription's orbit test.

theorem Hex.GraphIso.Nauty.childKey_of_ptrIter {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {gens : List (Array Nat)} {orbits : Array Nat} (hv : ∀ (γ : Array Nat), γ ∈ gens → checkAutom ctx.g γ = true) (tcLevel fuel level : Nat) {rsLab rsPtn : Array Nat} {tc lenT numcells o o' k : 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) (ho' : o' < lenT) (hlf : level + 1 + fuel ≤ n + 1) (hsound : OrbSound (OrbConn gens n) orbits n) (hptr : ptrIter orbits rsLab[tc + o]! k = rsLab[tc + o']!) : childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o = childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o'

A skipped child repeats the key at the end of its pointer chase. The chase is what reaches an orbit representative, which is the offset the loop actually explored, so this is the form the domination step applies.