def Hex.PermGroup.Primitivity.check {n : Nat} (G : Group n) (a : Fin n) (traces : Vector (List (Fin n × Fin n)) n) : Bool

Replay every off-diagonal seeded test. Omitting a test cannot certify primitivity, even when all traces that remain are individually valid.

Equations

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

theorem Hex.PermGroup.Primitivity.check_sound {n : Nat} {G : Group n} {a : Fin n} {traces : Vector (List (Fin n × Fin n)) n} (hn : 2 ≤ n) (ht : G.isTransitive = true) (h : check G a traces = true) : G.IsPrimitive

inductive Hex.PermGroup.Primitivity.Verdict {n : Nat} (G : Group n) : Type

Every verdict contains a complete reason: a degree obstruction, unreachable point, nontrivial invariant partition, or all seeded block certificates.

• small {n : Nat} {G : Group n} (degree : n < 2) : Verdict G
• intransitive {n : Nat} {G : Group n} (source target : Fin n) (missing : ¬target ∈ G.orbit source) : Verdict G
• imprimitive {n : Nat} {G : Group n} (point : Fin n) (failure : Failure G point) : Verdict G
• primitive {n : Nat} {G : Group n} (degree : 2 ≤ n) (transitive : G.isTransitive = true) (point : Fin n) (checks : Checks G point n ⋯) : Verdict G

def Hex.PermGroup.Primitivity.Verdict.accepted {n✝ : Nat} {G : Group n✝} (v : Verdict G) : Bool

Extract the Boolean decision without discarding the separately available certificate or obstruction.

Equations

• (Hex.PermGroup.Primitivity.Verdict.primitive degree transitive point checks).accepted = true
• v.accepted = false

theorem Hex.PermGroup.Primitivity.Verdict.accepted_iff {n : Nat} {G : Group n} (v : Verdict G) : v.accepted = true ↔ G.IsPrimitive

def Hex.PermGroup.Primitivity.decide {n : Nat} (G : Group n) : Verdict G

Decide transitivity at point zero, then perform the complete seeded criterion. Neither degree zero nor degree one enters the block search.

Equations

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

def Hex.PermGroup.Group.primitivity {n : Nat} (G : Group n) : Primitivity.Verdict G

A complete primitivity certificate or an explicit obstruction.

Equations

• G.primitivity = Hex.PermGroup.Primitivity.decide G

def Hex.PermGroup.Group.isPrimitive {n : Nat} (G : Group n) : Bool

Primitive means transitive of degree at least two, with no nontrivial invariant partition. The certificate remains available through primitivity.

Equations

• G.isPrimitive = G.primitivity.accepted

theorem Hex.PermGroup.Group.isPrimitive_iff {n : Nat} (G : Group n) : G.isPrimitive = true ↔ G.IsPrimitive