def Hex.PermGroup.Kernel.rarrayOf {α : Type} [Inhabited α] (xs : Array α) : Lean.RArray α

A balanced RArray holding xs[j] at index j, for nonempty xs.

Equations

• Hex.PermGroup.Kernel.rarrayOf xs = Hex.PermGroup.Kernel.rarrayOf.go✝ xs xs.size 0 xs.size

@[instance_reducible]

def Hex.PermGroup.Kernel.instInhabitedPerm {n : Nat} : Inhabited (Perm n)

Equations

• Hex.PermGroup.Kernel.instInhabitedPerm = { default := Hex.Perm.id n }

def Hex.PermGroup.Kernel.lcg (seed : Nat) : Nat

One step of a linear congruential generator, for deterministic sampling.

Equations

• Hex.PermGroup.Kernel.lcg seed = (seed * 6364136223846793005 + 1442695040888963407) % 2 ^ 64

def Hex.PermGroup.Kernel.orbitTree {n : Nat} (gens : Array (Perm n)) (b : Fin n) : Array (Fin n) × Array (Nat × Nat) × Array (Perm n)

The orbit of b under gens in breadth-first order. Each later point records its Schreier-tree edge (i, k), meaning point j is gens[i] applied to point k < j, and its transversal element.

Equations

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

def Hex.PermGroup.Kernel.extendAll {n : Nat} (c : (T : Array (Perm n)) × Construction T 0) (gens : Array (Perm n)) : (T : Array (Perm n)) × Construction T 0

Add generators to a complete chain by extension, skipping those it already contains.

Equations

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

def Hex.PermGroup.Kernel.orderOf {n : Nat} (gens : Array (Perm n)) : Nat

The order of the group generated by gens, from a complete chain built by extension only. Such chains are not stored in groups, but their orbit sizes give the order.

Equations

• Hex.PermGroup.Kernel.orderOf gens = (Hex.PermGroup.Kernel.extendAll ⟨#[], Hex.PermGroup.Build.empty 0 ⋯⟩ gens).snd.chain.orbitProduct

def Hex.PermGroup.Kernel.orbitRoots {n : Nat} (gens : Array (Perm n)) : Array Nat

The orbit partition of gens, as the least point of each point's orbit.

Equations

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

structure Hex.PermGroup.Kernel.PartialChain (n : Nat) : Type

A partial stabilizer chain built from elements of a group H: base points, the generators added at each level (level i uses those of levels ≥ i, all of which fix the earlier base points), and each level's transversal, indexed by point. Each level's orbit lies in the orbit of its base point under the corresponding point stabilizer of H, so the product of the orbit sizes is at most |H|, whether or not the chain is complete.

• bases : Array (Fin n)
• strong : Array (Array (Perm n))
• trans : Array (Array (Option (Perm n)))

def Hex.PermGroup.Kernel.PartialChain.bound {n : Nat} (c : PartialChain n) : Nat

The orbit sizes' product, a lower bound on the order of the group.

Equations

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

def Hex.PermGroup.Kernel.PartialChain.transversal {n : Nat} (gens : Array (Perm n)) (b : Fin n) : Array (Option (Perm n))

The transversal of b under gens, by breadth-first search.

Equations

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

def Hex.PermGroup.Kernel.PartialChain.refresh {n : Nat} (c : PartialChain n) (i : Nat) : PartialChain n

Recompute the transversals of levels 0 to i.

Equations

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

def Hex.PermGroup.Kernel.PartialChain.add {n : Nat} (c : PartialChain n) (g : Perm n) : PartialChain n

Sift g, adding its residue as a new generator when it is not the identity.

Equations

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

def Hex.PermGroup.Kernel.reachesOrder {n : Nat} (gens : Array (Perm n)) (target seed : Nat) (patience : Nat := 40) : Bool

Whether the group generated by gens, known to lie in a group of order target, is all of it: sift pseudo-random elements of the group, made by product replacement, into a partial chain until its lower bound reaches target. Stops with false after patience consecutive elements that do not raise the bound, or after 100000 elements. A true answer is certain; false does not show that gens fails to generate.

Equations

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

def Hex.PermGroup.Kernel.product {n : Nat} (cands : Array (Perm n)) (w : List Nat) : Perm n

The product of the candidates at the given indices, leftmost outermost.

Equations

• Hex.PermGroup.Kernel.product cands w = List.foldr (fun (i : Nat) (p : Hex.Perm n) => cands[i]!.comp p) (Hex.Perm.id n) w

def Hex.PermGroup.Kernel.smallGenerating {n : Nat} (cands : Array (Perm n)) (target seed start : Nat) (wordLength : Nat := 3) (greedy : Bool := true) : List (List Nat)

A few products of elements of cands, as index lists, generating a group of order target. A single candidate of order target is taken if there is one. Otherwise pseudo-random sets of start (clamped to two or three) up to three products of three candidates are tried, each first compared on orbits and then accepted when reachesOrder shows that it generates a group of order target. Failing those, candidates are added singly, in order, whenever they enlarge the group.

Equations

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

def Hex.PermGroup.Kernel.certLevels (n a✝ : Nat) : Array (Perm n) → Nat → Nat → Except String Certificate

The levels of a certificate for the group of order order generated by the non-identity permutations gens. Each level's base is the least point moved by its generators, and the next level's generators are a few of its Schreier generators that generate the stabilizer.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Kernel.certLevels n 0 x✝² x✝¹ x✝ = throw "certificate construction did not terminate"

def Hex.PermGroup.Kernel.certify {n : Nat} (S : Array (Perm n)) : Except String Certificate

The kernel certificate of the group generated by S. The first level's generators are a few products of the distinct non-identity inputs that generate the group, found by sampling sets of products of three and then of eight inputs, or those inputs themselves when sampling finds no smaller set.

Equations

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

def Hex.PermGroup.Kernel.siftCost (n : Nat) (rest : List Level) : Nat

Estimated kernel work, in field operations, of one sift through rest.

Equations

• Hex.PermGroup.Kernel.siftCost n rest = List.foldl (fun (acc : Nat) (L : Hex.PermGroup.Kernel.Level) => acc + n + L.size.log2 + 2) n rest

def Hex.PermGroup.Kernel.pairCost (n : Nat) (L : Level) (rest : List Level) : Nat

Estimated work of one Schreier pair of L followed by rest.

Equations

• Hex.PermGroup.Kernel.pairCost n L rest = 2 * n + L.size.log2 + Hex.PermGroup.Kernel.siftCost n rest

def Hex.PermGroup.Kernel.levelCost (n : Nat) (L : Level) (_rest : List Level) : Nat

Estimated work of levelOk for L followed by rest.

Equations

• Hex.PermGroup.Kernel.levelCost n L _rest = 2 * L.size + 2 * n + 3 * L.size * n + List.foldl (fun (acc : Nat) (w : List (Nat × Nat)) => acc + 3 * n * w.length + n) 0 L.next

def Hex.PermGroup.Kernel.inputsCost (n inputCount : Nat) (c : Certificate) : Nat

Estimated work of inputsOk.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Kernel.inputsCost n inputCount [] = inputCount * Hex.PermGroup.Kernel.siftCost n [] + 0

def Hex.PermGroup.Kernel.ranges (total step : Nat) : List (Nat × Nat)

Split [0, total) into adjacent ranges of at most step pairs.

Equations

• Hex.PermGroup.Kernel.ranges total step = List.map (fun (r : Nat) => (r * step, min total ((r + 1) * step))) (List.range ((total + step - 1) / step))

def Hex.PermGroup.Kernel.chunks (n inputCount : Nat) (c : Certificate) (budget : Nat) : Except String (List (List (Nat × Nat)))

For each level, adjacent ranges of Schreier pairs whose estimated work is at most budget, or the first check that cannot fit.

Equations

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