def Hex.PermGroup.Core.check {n : Nat} (G H K : Group n) (trace : List (Step n)) : Bool

Replay strict complete intersections and verify the final normality pass.

Equations

• Hex.PermGroup.Core.check G H K trace = match Hex.PermGroup.Core.replay G H trace with | none => false | some L => L.sameGroup K && Hex.PermGroup.Normal.check G K

theorem Hex.PermGroup.Core.check_spec {n : Nat} {G H K : Group n} {trace : List (Step n)} (h : check G H K trace = true) (p : Perm n) : Generated K.generators p ↔ Member G H p

structure Hex.PermGroup.Core.Result {n : Nat} (G H : Group n) : Type

Complete replay data certifies both containment and maximality.

• group : Group n
• trace : List (Step n)
• replayed : replay G H self.trace = some self.group
• normal : Normal.check G self.group = true

theorem Hex.PermGroup.Core.Result.checked {n : Nat} {G H : Group n} (c : Result G H) : check G H c.group c.trace = true

theorem Hex.PermGroup.Core.Result.spec {n : Nat} {G H : Group n} (c : Result G H) (p : Perm n) : Generated c.group.generators p ↔ Member G H p

theorem Hex.PermGroup.Core.Result.inside {n : Nat} {G H : Group n} (c : Result G H) : c.group.IsSubgroup H

theorem Hex.PermGroup.Core.Result.greatest {n : Nat} {G H : Group n} (c : Result G H) (N : Group n) (hN : N.IsSubgroup H) (hn : Normal.check G N = true) : N.IsSubgroup c.group

theorem Hex.PermGroup.Core.Result.growth {n : Nat} {G H : Group n} (c : Result G H) : 2 ^ c.trace.length * c.group.order ≤ H.order

def Hex.PermGroup.Core.Result.prepend {n : Nat} {G H K : Group n} (s : Step n) (hs : step G H s = some K) (child : Result G K) : Result G H

Equations

• Hex.PermGroup.Core.Result.prepend s hs child = { group := child.group, trace := s :: child.trace, replayed := ⋯, normal := ⋯ }

def Hex.PermGroup.Core.cut {n : Nat} (G H : Group n) (i : Fin G.chain.generators.size) : Search.Solution (Search.Intersection.constraint H (Group.conjugate G.chain.generators[↑i].inv H))

A complete intersection with the inverse conjugate named by a failed normality test. Its generators and search tree are retained for replay.

Equations

• Hex.PermGroup.Core.cut G H i = H.intersectionSearch (Hex.PermGroup.Group.conjugate G.chain.generators[↑i].inv H)

theorem Hex.PermGroup.Core.cut_spec {n : Nat} (G H : Group n) (i : Fin G.chain.generators.size) (p : Perm n) : Generated (cut G H i).group.generators p ↔ Generated H.generators p ∧ Generated H.generators (G.chain.generators[↑i].conj p)

theorem Hex.PermGroup.Core.cut_strict {n : Nat} (G H : Group n) (i : Fin G.chain.generators.size) (j : Fin H.generators.size) (hn : ¬Generated H.generators (G.chain.generators[↑i].conj H.generators[↑j])) : ¬SameGroup (cut G H i).group H

theorem Hex.PermGroup.Core.cut_step {n : Nat} (G H : Group n) (i : Fin G.chain.generators.size) (j : Fin H.generators.size) (hn : ¬Generated H.generators (G.chain.generators[↑i].conj H.generators[↑j])) : step G H { conjugator := ↑i, conjugate := (Group.conjugate G.chain.generators[↑i].inv H).chain, group := (cut G H i).group, certificate := (cut G H i).certificate } = some (cut G H i).group

theorem Hex.PermGroup.Core.cut_decreases {n : Nat} (G H : Group n) (i : Fin G.chain.generators.size) (j : Fin H.generators.size) (hn : ¬Generated H.generators (G.chain.generators[↑i].conj H.generators[↑j])) : (cut G H i).group.order < H.order

def Hex.PermGroup.Core.iterate {n : Nat} (G : Group n) (remaining : Nat) (H : Group n) (bound : H.order ≤ remaining) : Result G H

The order bound cannot be exhausted before the subgroup is normal.

Equations

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

def Hex.PermGroup.Core.build {n : Nat} (G H : Group n) : Result G H

Equations

• Hex.PermGroup.Core.build G H = Hex.PermGroup.Core.iterate G H.order H ⋯

def Hex.PermGroup.Group.coreCert {n : Nat} (G H : Group n) (_h : H.IsSubgroup G) : Core.Result G H

The greatest normal subgroup of G contained in H, with complete intersection certificates and a terminal normality check.

Equations

• G.coreCert H _h = Hex.PermGroup.Core.build G H

def Hex.PermGroup.Group.core {n : Nat} (G H : Group n) (h : H.IsSubgroup G) : Group n

Equations

• G.core H h = (G.coreCert H h).group

theorem Hex.PermGroup.Group.mem_core {n : Nat} (G H : Group n) (h : H.IsSubgroup G) (p : Perm n) : Generated (G.core H h).generators p ↔ ∀ (g : Perm n), Generated G.generators g → Generated H.generators (g.conj p)

theorem Hex.PermGroup.Group.core_inside {n : Nat} (G H : Group n) (h : H.IsSubgroup G) : (G.core H h).IsSubgroup H

theorem Hex.PermGroup.Group.core_subgroup {n : Nat} (G H : Group n) (h : H.IsSubgroup G) : (G.core H h).IsSubgroup G

theorem Hex.PermGroup.Group.core_normal {n : Nat} (G H : Group n) (h : H.IsSubgroup G) : (G.core H h).isNormal G ⋯ = true

theorem Hex.PermGroup.Group.le_core {n : Nat} (G H N : Group n) (h : H.IsSubgroup G) (hn : Normal.check G N = true) : N.IsSubgroup (G.core H h) ↔ N.IsSubgroup H