structure Hex.PermGroup.Orbit.Tree {n : Nat} (S : Array (Perm n)) (a : Fin n) : Type

A discovery tree. Parent edges refer to earlier entries and retain the generator's input index. Lookup entries use natural numbers during construction, so appending a point does not traverse the lookup vector to cast indices.

• points : Array (Fin n)
• lookup : Vector (Option Nat) n
• parents : Vector (Option (Nat × Fin S.size)) self.points.size
• nodup : self.points.toList.Nodup
• base : a ∈ self.points
• lookup_point (j : Fin self.points.size) : self.lookup[↑self.points[↑j]] = some ↑j
• point_lookup (x : Fin n) (j : Nat) : self.lookup[↑x] = some j → ∃ (h : j < self.points.size), self.points[j] = x
• edge (j : Fin self.points.size) : match self.parents[↑j] with | none => self.points[↑j] = a | some (k, i) => ∃ (h : k < ↑j), S[↑i].get self.points[k] = self.points[↑j]

def Hex.PermGroup.Orbit.Tree.root {n : Nat} (S : Array (Perm n)) (a : Fin n) : Tree S a

Start the queue with its root.

Equations

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

theorem Hex.PermGroup.Orbit.Tree.missing {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (x : Fin n) : t.lookup[↑x] = none ↔ ¬x ∈ t.points

theorem Hex.PermGroup.Orbit.Tree.size_le {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) : t.points.size ≤ n

theorem Hex.PermGroup.Orbit.Tree.size_pos {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) : 0 < t.points.size

theorem Hex.PermGroup.Orbit.Tree.point_zero {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) : t.points[0] = a

theorem Hex.PermGroup.Orbit.Tree.base_parent {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) (hj : t.points[↑j] = a) : t.parents[↑j] = none

theorem Hex.PermGroup.Orbit.Tree.reachable {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) : ∃ (p : Perm n), Generated S p ∧ p.get a = t.points[↑j]

Following parent edges gives a generated transporter, independently of any program encoding used to export the discovery tree.

def Hex.PermGroup.Orbit.Tree.push {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) (i : Fin S.size) (hnew : ¬S[↑i].get t.points[↑j] ∈ t.points) : Tree S a

Append a previously unseen neighbor and its parent edge.

Equations

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

structure Hex.PermGroup.Orbit.Tree.Extends {n : Nat} {S : Array (Perm n)} {a : Fin n} (t u : Tree S a) : Prop

Extension preserves queue indices as well as membership.

• size : t.points.size ≤ u.points.size
• get (j : Fin t.points.size) : u.points[↑j] = t.points[↑j]

theorem Hex.PermGroup.Orbit.Tree.Extends.refl {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) : t.Extends t

theorem Hex.PermGroup.Orbit.Tree.Extends.trans {n : Nat} {S : Array (Perm n)} {a : Fin n} {t u v : Tree S a} (htu : t.Extends u) (huv : u.Extends v) : t.Extends v

theorem Hex.PermGroup.Orbit.Tree.Extends.mem {n : Nat} {S : Array (Perm n)} {a : Fin n} {t u : Tree S a} (h : t.Extends u) {x : Fin n} (hx : x ∈ t.points) : x ∈ u.points

theorem Hex.PermGroup.Orbit.Tree.push_extends {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) (i : Fin S.size) (hnew : ¬S[↑i].get t.points[↑j] ∈ t.points) : t.Extends (t.push j i hnew)

def Hex.PermGroup.Orbit.Tree.visit {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) (i : Fin S.size) : Tree S a

Inspect one directed edge, appending its target only on first discovery.

Equations

• t.visit j i = if h : t.lookup[↑(S[↑i].get t.points[↑j])] = none then t.push j i ⋯ else t

theorem Hex.PermGroup.Orbit.Tree.visit_extends {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) (i : Fin S.size) : t.Extends (t.visit j i)

theorem Hex.PermGroup.Orbit.Tree.visit_mem {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) (i : Fin S.size) : S[↑i].get t.points[↑j] ∈ (t.visit j i).points

def Hex.PermGroup.Orbit.Tree.scan {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) (gs : List (Fin S.size)) : Tree S a

Inspect the generators in their supplied order. Recursive calls carry the same parent index through the growing queue.

Equations

• t.scan j [] = t
• t.scan j (i :: gs_2) = (t.visit j i).scan ⟨↑j, ⋯⟩ gs_2

theorem Hex.PermGroup.Orbit.Tree.scan_extends {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) (gs : List (Fin S.size)) : t.Extends (t.scan j gs)

theorem Hex.PermGroup.Orbit.Tree.scan_mem {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) (gs : List (Fin S.size)) (i : Fin S.size) (hi : i ∈ gs) : S[↑i].get t.points[↑j] ∈ (t.scan j gs).points

def Hex.PermGroup.Orbit.Tree.Processed {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (cursor : Nat) : Prop

The first cursor queue entries have had all their edges inspected.

Equations

• t.Processed cursor = ∀ (j : Fin t.points.size), ↑j < cursor → ∀ (i : Fin S.size), S[↑i].get t.points[↑j] ∈ t.points

theorem Hex.PermGroup.Orbit.Tree.scan_processed {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (cursor : Nat) (hc : cursor < t.points.size) (hp : t.Processed cursor) : (t.scan ⟨cursor, hc⟩ (List.finRange S.size)).Processed (cursor + 1)

@[irreducible]

def Hex.PermGroup.Orbit.Tree.finish {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (cursor : Nat) (hp : t.Processed cursor) : { u : Tree S a // t.Extends u ∧ u.Processed u.points.size }

Process each discovered point exactly once. Termination uses the degree, with the duplicate-free queue proving that no more than n points are visited.

Equations

• t.finish cursor hp = if hc : cursor < t.points.size then let r := t.scan ⟨cursor, hc⟩ (List.finRange S.size); let result := r.finish (cursor + 1) ⋯; ⟨result.val, ⋯⟩ else ⟨t, ⋯⟩

def Hex.PermGroup.Orbit.breadthFirst {n : Nat} (S : Array (Perm n)) (a : Fin n) : { t : Tree S a // t.Processed t.points.size }

Deterministic breadth-first discovery with constant-time point lookup and parent edges. Every generator edge from the returned point set stays in it.

Equations

• Hex.PermGroup.Orbit.breadthFirst S a = ⟨((Hex.PermGroup.Orbit.Tree.root S a).finish 0 ⋯).val, ⋯⟩