structure Hex.PermGroup.Group (n : Nat) : Type

A finite permutation group with an independently checked complete chain. The original ordered generator array is retained for membership programs.

• generators : Array (Perm n)
• chain : Chain n
• valid : checkChain self.generators self.chain = true

def Hex.PermGroup.Group.ofChain? {n : Nat} (S : Array (Perm n)) (c : Chain n) : Option (Group n)

Validate raw chain data before exposing any group decision or exact order.

Equations

• Hex.PermGroup.Group.ofChain? S c = if h : Hex.PermGroup.checkChain S c = true then some { generators := S, chain := c, valid := h } else none

@[simp]

theorem Hex.PermGroup.Group.isSome_ofChain? {n : Nat} (S : Array (Perm n)) (c : Chain n) : (ofChain? S c).isSome = checkChain S c

def Hex.PermGroup.Group.contains {n : Nat} (G : Group n) (p : Perm n) : Bool

Exact membership, including replayable negative sifts.

Equations

• G.contains p = G.chain.accepts 0 p

theorem Hex.PermGroup.Group.contains_iff {n : Nat} (G : Group n) (p : Perm n) : G.contains p = true ↔ Generated G.generators p

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

Exact order from the complete chain, using arbitrary-precision naturals.

Equations

• G.order = G.chain.orbitProduct

theorem Hex.PermGroup.Group.order_pos {n : Nat} (G : Group n) : 0 < G.order

def Hex.PermGroup.SameGroup {n : Nat} (G H : Group n) : Prop

Mathematical equality of represented subgroups, independent of their ordered generators, certificates, or Lean record equality.

Equations

• Hex.PermGroup.SameGroup G H = ∀ (p : Hex.Perm n), Hex.PermGroup.Generated G.generators p ↔ Hex.PermGroup.Generated H.generators p

@[reducible, inline]

abbrev Hex.PermGroup.Element {n : Nat} (G : Group n) : Type

An element's identity is its permutation value. A membership word is separate certificate data and does not enter equality.

Equations

• Hex.PermGroup.Element G = { p : Hex.Perm n // Hex.PermGroup.Generated G.generators p }

def Hex.PermGroup.Element.ofPerm? {n : Nat} (G : Group n) (p : Perm n) : Option (Element G)

Construct an element from a raw permutation exactly when it belongs to the group.

Equations

• Hex.PermGroup.Element.ofPerm? G p = if h : G.contains p = true then some ⟨p, ⋯⟩ else none

@[simp]

theorem Hex.PermGroup.Element.isSome_ofPerm? {n : Nat} (G : Group n) (p : Perm n) : (ofPerm? G p).isSome = G.contains p

def Hex.PermGroup.Element.id {n : Nat} (G : Group n) : Element G

Equations

• Hex.PermGroup.Element.id G = ⟨Hex.Perm.id n, ⋯⟩

def Hex.PermGroup.Element.comp {n : Nat} {G : Group n} (p q : Element G) : Element G

Equations

• p.comp q = ⟨p.val.comp q.val, ⋯⟩

def Hex.PermGroup.Element.inv {n : Nat} {G : Group n} (p : Element G) : Element G

Equations

• p.inv = ⟨p.val.inv, ⋯⟩

@[instance_reducible]

instance Hex.PermGroup.Element.instMul {n : Nat} {G : Group n} : Mul (Element G)

Equations

• Hex.PermGroup.Element.instMul = { mul := Hex.PermGroup.Element.comp }

@[instance_reducible]

instance Hex.PermGroup.Element.instInv {n : Nat} {G : Group n} : Inv (Element G)

Equations

• Hex.PermGroup.Element.instInv = { inv := Hex.PermGroup.Element.inv }

@[instance_reducible]

instance Hex.PermGroup.Element.instOfNatOfNatNat {n : Nat} {G : Group n} : OfNat (Element G) 1

Equations

• Hex.PermGroup.Element.instOfNatOfNatNat = { ofNat := Hex.PermGroup.Element.id G }

@[simp]

theorem Hex.PermGroup.Element.val_id {n : Nat} {G : Group n} : (Element.id G).val = Perm.id n

@[simp]

theorem Hex.PermGroup.Element.val_comp {n : Nat} {G : Group n} (p q : Element G) : (p.comp q).val = p.val.comp q.val

@[simp]

theorem Hex.PermGroup.Element.val_inv {n : Nat} {G : Group n} (p : Element G) : p.inv.val = p.val.inv

@[simp]

theorem Hex.PermGroup.Element.comp_id {n : Nat} {G : Group n} (p : Element G) : p.comp (Element.id G) = p

@[simp]

theorem Hex.PermGroup.Element.id_comp {n : Nat} {G : Group n} (p : Element G) : (Element.id G).comp p = p

theorem Hex.PermGroup.Element.comp_assoc {n : Nat} {G : Group n} (p q r : Element G) : (p.comp q).comp r = p.comp (q.comp r)

@[simp]

theorem Hex.PermGroup.Element.comp_inv_self {n : Nat} {G : Group n} (p : Element G) : p.comp p.inv = Element.id G

@[simp]

theorem Hex.PermGroup.Element.inv_comp_self {n : Nat} {G : Group n} (p : Element G) : p.inv.comp p = Element.id G