def Hex.PermGroup.Search.Sets.cardinality {n : Nat} (A : Vector Bool n) : Nat

Equations

• Hex.PermGroup.Search.Sets.cardinality A = List.countP A.get (List.finRange n)

theorem Hex.PermGroup.Search.Sets.cardinality_eq {n : Nat} (A B : Vector Bool n) (p : Perm n) (h : test A B p = true) : cardinality A = cardinality B

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

A cardinality mismatch excludes all permutations, before any chain traversal; other reasons identify a violated partial-image constraint.

• cardinality {n : Nat} : TransportReason n
• refinement {n : Nat} (reason : Reason n) : TransportReason n

def Hex.PermGroup.Search.Sets.transporter {n : Nat} (G : Group n) (A B : Vector Bool n) : Pruner G (test A B)

Equations

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

def Hex.PermGroup.Group.setTransporterSearch {n : Nat} (G : Group n) (A B : Vector Bool n) : Search.Answer (Search.Sets.transporter G A B)

A checked transporter word or a complete failure certificate. The source and target subsets need not be in the same orbit.

Equations

• G.setTransporterSearch A B = Hex.PermGroup.Search.first (Hex.PermGroup.Search.Sets.transporter G A B)

def Hex.PermGroup.Group.setTransporter? {n : Nat} (G : Group n) (A B : Vector Bool n) : Option (Element G)

Equations

• G.setTransporter? A B = Hex.PermGroup.Search.Answer.element? (Hex.PermGroup.Search.Sets.transporter G A B) (G.setTransporterSearch A B)

theorem Hex.PermGroup.Group.setTransporter_image {n : Nat} (G : Group n) (A B : Vector Bool n) (p : Element G) (h : G.setTransporter? A B = some p) : (Action.subsets G).act p A = B

theorem Hex.PermGroup.Group.setTransporter_none {n : Nat} (G : Group n) (A B : Vector Bool n) : G.setTransporter? A B = none ↔ ¬∃ (p : Element G), (Action.subsets G).act p A = B

theorem Hex.PermGroup.Group.setTransporter_cardinality {n : Nat} (G : Group n) (A B : Vector Bool n) (h : Search.Sets.cardinality A ≠ Search.Sets.cardinality B) : G.setTransporter? A B = none

theorem Hex.PermGroup.Group.mem_transporter_coset {n : Nat} (G : Group n) (A B : Vector Bool n) (t : Element G) (ht : (Action.subsets G).act t A = B) (p : Perm n) : Generated (G.setStabilizer A).generators (t.val.inv.comp p) ↔ Generated G.generators p ∧ Search.Sets.test A B p = true

The relative permutation to any one transporter lies in the source set stabilizer exactly when the original permutation is another transporter.

theorem Hex.PermGroup.Group.setTransporter_coset {n : Nat} (G : Group n) (A B : Vector Bool n) (t p : Element G) (ht : (Action.subsets G).act t A = B) : (Action.subsets G).act p A = B ↔ ∃ (k : Element (G.setStabilizer A)), p.val = t.val.comp k.val

All transporters are the left coset t * setStabilizer G A, with the same multiplication order as the executable action.