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

Transporter roots for the first k discovery entries, sharing an append-only program. Bounds and transporter invariants are erased during compilation.

• arena : Program.Builder S
• roots : Vector Nat k
• size : k ≤ t.points.size
• bound (j : Fin k) : self.roots[↑j] < self.arena.values.size
• image (j : Fin k) : self.arena.values[self.roots[↑j]].val.get a = t.points[↑j]
• identity (j : Fin k) : t.points[↑j] = a → self.arena.values[self.roots[↑j]].val = Perm.id n

def Hex.PermGroup.Orbit.Tree.Certificates.empty {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) : t.Certificates 0

Equations

• Hex.PermGroup.Orbit.Tree.Certificates.empty t = { arena := Hex.PermGroup.Program.Builder.empty S, roots := #v[], size := ⋯, bound := ⋯, image := ⋯, identity := ⋯ }

def Hex.PermGroup.Orbit.Tree.Certificates.append {n : Nat} {S : Array (Perm n)} {a : Fin n} {t : Tree S a} {k : Nat} (c : t.Certificates k) (hk : k < t.points.size) (b : Program.Builder S) (hs : c.arena.values.size ≤ b.values.size) (he : ∀ (j : Fin c.arena.values.size), b.values[↑j] = c.arena.values[↑j]) (r : Fin b.values.size) (hi : b.values[↑r].val.get a = t.points[k]) (hid : t.points[k] = a → b.values[↑r].val = Perm.id n) : t.Certificates (k + 1)

Retain earlier roots when the arena grows, then append one new transporter.

Equations

• c.append hk b hs he r hi hid = { arena := b, roots := c.roots.push ↑r, size := hk, bound := ⋯, image := ⋯, identity := ⋯ }

def Hex.PermGroup.Orbit.Tree.Certificates.next {n : Nat} {S : Array (Perm n)} {a : Fin n} {t : Tree S a} {k : Nat} (c : t.Certificates k) (hk : k < t.points.size) : t.Certificates (k + 1)

Compile one parent edge. The generator is composed on the left of its parent's transporter, using earlier node references rather than copied words.

Equations

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

@[irreducible]

def Hex.PermGroup.Orbit.Tree.Certificates.finish {n : Nat} {S : Array (Perm n)} {a : Fin n} {t : Tree S a} {k : Nat} (c : t.Certificates k) : t.Certificates t.points.size

Compile the remaining entries in discovery order.

Equations

• c.finish = if hk : k < t.points.size then (c.next hk).finish else cast ⋯ c

theorem Hex.PermGroup.Orbit.Tree.Certificates.next_size {n : Nat} {S : Array (Perm n)} {a : Fin n} {t : Tree S a} {k : Nat} (c : t.Certificates k) (hk : k < t.points.size) : (c.next hk).arena.values.size ≤ c.arena.values.size + 2

theorem Hex.PermGroup.Orbit.Tree.Certificates.finish_size {n : Nat} {S : Array (Perm n)} {a : Fin n} {t : Tree S a} {k : Nat} (c : t.Certificates k) : c.finish.arena.values.size ≤ c.arena.values.size + 2 * (t.points.size - k)

Compiling a tree adds at most two nodes per point, regardless of path length.

theorem Hex.PermGroup.Orbit.Tree.Certificates.nodes_le {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) : (empty t).finish.arena.nodes.size ≤ 2 * t.points.size

def Hex.PermGroup.Orbit.Tree.Certificates.lookup {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (x : Fin n) : Option (Fin t.points.size)

Convert natural lookup indices to bounded indices once, after discovery.

Equations

• Hex.PermGroup.Orbit.Tree.Certificates.lookup t x = match h : t.lookup[↑x] with | none => none | some j => some ⟨j, ⋯⟩

theorem Hex.PermGroup.Orbit.Tree.Certificates.lookup_point {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (j : Fin t.points.size) : lookup t t.points[↑j] = some j

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

theorem Hex.PermGroup.Orbit.Tree.Certificates.point_lookup {n : Nat} {S : Array (Perm n)} {a : Fin n} (t : Tree S a) (x : Fin n) (j : Fin t.points.size) (h : lookup t x = some j) : t.points[↑j] = x

def Hex.PermGroup.Orbit.Tree.Certificates.orbit {n : Nat} {S : Array (Perm n)} {a : Fin n} {t : Tree S a} (c : t.Certificates t.points.size) : Orbit n

All emitted words share the completed arena's node array.

Equations

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

theorem Hex.PermGroup.Orbit.Tree.Certificates.valid {n : Nat} {S : Array (Perm n)} {a : Fin n} {t : Tree S a} (c : t.Certificates t.points.size) (ht : t.Processed t.points.size) (hs : ∀ (p : Perm n), p ∈ S → p.inv ∈ S) : Valid S a c.orbit

def Hex.PermGroup.Orbit.ofSymmetric {n : Nat} (S : Array (Perm n)) (a : Fin n) (hs : ∀ (p : Perm n), p ∈ S → p.inv ∈ S) : { c : Orbit n // Valid S a c }

Construct a checked orbit for an inverse-closed generator array, retaining its order and indices in the discovery edges and transporter programs.

Equations

• Hex.PermGroup.Orbit.ofSymmetric S a hs = ⟨(Hex.PermGroup.Orbit.Tree.Certificates.empty (Hex.PermGroup.Orbit.breadthFirst S a).val).finish.orbit, ⋯⟩

theorem Hex.PermGroup.Orbit.ofSymmetric_checks {n : Nat} (S : Array (Perm n)) (a : Fin n) (hs : ∀ (p : Perm n), p ∈ S → p.inv ∈ S) : checkOrbit S a (ofSymmetric S a hs).val = true