structure Hex.PermGroup.Primitivity.Checks {n : Nat} (G : Group n) (a : Fin n) (k : Nat) (hk : k ≤ n) : Type

The first k seed tests have complete forced-union traces. The diagonal test is vacuous and uses an empty trace without running a block search.

• traces : Vector (List (Fin n × Fin n)) k
• checked (i : Fin k) : let b := ⟨↑i, ⋯⟩; b ≠ a → Blocks.check G.chain.generators [(a, b)] (Partition.indiscrete n) self.traces[↑i] = true

structure Hex.PermGroup.Primitivity.Failure {n : Nat} (G : Group n) (a : Fin n) : Type

A checked invariant partition that is neither discrete nor indiscrete.

• point : Fin n
• distinct : self.point ≠ a
• solution : Blocks.Solution G.chain.generators [(a, self.point)]
• proper : self.solution.partition ≠ Partition.indiscrete n

theorem Hex.PermGroup.Primitivity.Failure.invariant {n : Nat} {G : Group n} {a : Fin n} (f : Failure G a) : f.solution.partition.IsInvariant G

theorem Hex.PermGroup.Primitivity.Failure.nondiscrete {n : Nat} {G : Group n} {a : Fin n} (f : Failure G a) : f.solution.partition ≠ Partition.discrete n

theorem Hex.PermGroup.Primitivity.Failure.not_primitive {n : Nat} {G : Group n} {a : Fin n} (f : Failure G a) : ¬G.IsPrimitive

inductive Hex.PermGroup.Primitivity.Result {n : Nat} (G : Group n) (a : Fin n) (k : Nat) (hk : k ≤ n) : Type

Either all tests through k are complete, or an explicit nontrivial invariant partition has been found.

• complete {n : Nat} {G : Group n} {a : Fin n} {k : Nat} {hk : k ≤ n} (checks : Checks G a k hk) : Result G a k hk
• imprimitive {n : Nat} {G : Group n} {a : Fin n} {k : Nat} {hk : k ≤ n} (failure : Failure G a) : Result G a k hk

def Hex.PermGroup.Primitivity.Checks.push {n : Nat} {G : Group n} {a : Fin n} {k : Nat} {hk : k ≤ n} (c : Checks G a k hk) (hn : k + 1 ≤ n) (trace : List (Fin n × Fin n)) (h : have b := ⟨k, ⋯⟩; b ≠ a → Blocks.check G.chain.generators [(a, b)] (Partition.indiscrete n) trace = true) : Checks G a (k + 1) hn

Append one successful seed test to the already checked prefix.

Equations

• c.push hn trace h = { traces := c.traces.push trace, checked := ⋯ }

theorem Hex.PermGroup.Primitivity.Checks.criterion {n : Nat} {G : Group n} {a : Fin n} (c : Checks G a n ⋯) (b : Fin n) : b ≠ a → G.blocks [(a, b)] = Partition.indiscrete n

Complete traces prove the seeded criterion without rerunning the producer.

def Hex.PermGroup.Primitivity.scan {n : Nat} (G : Group n) (a : Fin n) (k : Nat) (hk : k ≤ n) : Result G a k hk

Visit other points in natural order, retaining each completed block trace and stopping immediately at a nontrivial invariant partition.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Primitivity.scan G a 0 hk_2 = Hex.PermGroup.Primitivity.Result.complete { traces := #v[], checked := ⋯ }