def Hex.PermGroup.Search.Sets.test {n : Nat} (A B : Vector Bool n) (p : Perm n) : Bool

Forward images preserve the prescribed source and target membership colors.

Equations

• Hex.PermGroup.Search.Sets.test A B p = decide (∀ (x : Fin n), A.get x = B.get (p.get x))

theorem Hex.PermGroup.Search.Sets.test_action {n : Nat} (G : Group n) (A B : Vector Bool n) (p : Element G) : test A B p.val = true ↔ (Action.subsets G).act p A = B

def Hex.PermGroup.Search.Predicate.setStabilizer {n : Nat} (A : Vector Bool n) : Predicate n

Equations

• Hex.PermGroup.Search.Predicate.setStabilizer A = { test := Hex.PermGroup.Search.Sets.test A A, id := ⋯, comp := ⋯, inv := ⋯ }

theorem Hex.PermGroup.Search.Sets.orbit_count {n : Nat} {G : Group n} (A B : Vector Bool n) (t : Node G) (p : Perm n) (hp : t.Contains p) (h : test A B p = true) (x : Fin n) : List.countP A.get (t.orbit x).toList = List.countP (fun (y : Fin n) => B.get (t.rep.val.get y)) (t.orbit x).toList

Counts are taken over a suffix orbit and its prefix image. A completion only permutes that orbit, so it cannot repair a mismatch between the counts.

inductive Hex.PermGroup.Search.Sets.Reason (n : Nat) : Type

• color {n : Nat} (x : Fin n) : Reason n
• orbit {n : Nat} (x : Fin n) : Reason n

def Hex.PermGroup.Search.Sets.reject {n : Nat} {G : Group n} (A B : Vector Bool n) (t : Node G) : Reason n → Bool

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Search.Sets.reject A B t (Hex.PermGroup.Search.Sets.Reason.color x_1) = (decide (↑x_1 < t.base) && decide (A.get x_1 ≠ B.get (t.rep.val.get x_1)))

theorem Hex.PermGroup.Search.Sets.reject_sound {n : Nat} {G : Group n} (A B : Vector Bool n) (t : Node G) (r : Reason n) (hr : reject A B t r = true) (p : Perm n) (hp : t.Contains p) : test A B p = false

def Hex.PermGroup.Search.Sets.trials (n : Nat) : Trials (Reason n)

Assigned colors are tested before orbit counts, in source-point order, without allocating all candidate reasons before testing the first.

Equations

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

def Hex.PermGroup.Search.Sets.find {n : Nat} {G : Group n} (A B : Vector Bool n) (t : Node G) : Option (Reason n)

Equations

• Hex.PermGroup.Search.Sets.find A B t = (Hex.PermGroup.Search.Sets.trials n).find (Hex.PermGroup.Search.Sets.reject A B t)

theorem Hex.PermGroup.Search.Sets.find_checked {n : Nat} {G : Group n} (A B : Vector Bool n) (t : Node G) (r : Reason n) (h : find A B t = some r) : reject A B t r = true

def Hex.PermGroup.Search.Sets.constraint {n : Nat} (G : Group n) (A : Vector Bool n) : Constraint G (Predicate.setStabilizer A)

Equations

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

def Hex.PermGroup.Group.setStabilizerSearch {n : Nat} (G : Group n) (A : Vector Bool n) : Search.Solution (Search.Sets.constraint G A)

Equations

• G.setStabilizerSearch A = Hex.PermGroup.Search.solve (Hex.PermGroup.Search.Sets.constraint G A)

def Hex.PermGroup.Group.setStabilizer {n : Nat} (G : Group n) (A : Vector Bool n) : Group n

Equations

• G.setStabilizer A = (G.setStabilizerSearch A).group

theorem Hex.PermGroup.Group.mem_setStabilizer {n : Nat} (G : Group n) (A : Vector Bool n) (p : Perm n) : Generated (G.setStabilizer A).generators p ↔ Generated G.generators p ∧ ∀ (x : Fin n), A.get x = A.get (p.get x)

theorem Hex.PermGroup.Group.setStabilizer_constant {n : Nat} (G : Group n) (value : Bool) : SameGroup (G.setStabilizer (Vector.replicate n value)) G

Both empty and full subsets are stabilized by the whole group.