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

A complete normal-closure certificate. The insertion trace reconstructs the generated subgroup; a terminal full pass verifies normality.

Equations

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

theorem Hex.PermGroup.Normal.checkClosure_spec {n : Nat} {G H K : Group n} {trace : List (Step n)} (hH : H.IsSubgroup G) (h : checkClosure G H K trace = true) : K.IsSubgroup G ∧ H.IsSubgroup K ∧ check G K = true ∧ ∀ (N : Group n), H.IsSubgroup N → check G N = true → K.IsSubgroup N

structure Hex.PermGroup.Normal.Closure {n : Nat} (G H : Group n) : Type

Exact output and raw chains for every strict conjugate insertion.

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

theorem Hex.PermGroup.Normal.Closure.checked {n : Nat} {G H : Group n} (c : Closure G H) : checkClosure G H c.group c.trace = true

theorem Hex.PermGroup.Normal.Closure.inside {n : Nat} {G H : Group n} (c : Closure G H) (hH : H.IsSubgroup G) : c.group.IsSubgroup G

theorem Hex.PermGroup.Normal.Closure.contains {n : Nat} {G H : Group n} (c : Closure G H) : H.IsSubgroup c.group

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

theorem Hex.PermGroup.Normal.Closure.growth {n : Nat} {G H : Group n} (c : Closure G H) (hH : H.IsSubgroup G) : 2 ^ c.trace.length * H.order ≤ G.order

Exact order bounds the number of strict chain rebuilds logarithmically.

def Hex.PermGroup.Normal.Closure.prepend {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])) (child : Closure G (H.adjoin (G.chain.generators[↑i].conj H.generators[↑j]))) : Closure G H

Prepend a certified strict conjugate insertion to the remaining closure.

Equations

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

theorem Hex.PermGroup.Normal.adjoin_decreases {n : Nat} (G H : Group n) (hH : H.IsSubgroup G) (i : Fin G.chain.generators.size) (j : Fin H.generators.size) (hn : ¬Generated H.generators (G.chain.generators[↑i].conj H.generators[↑j])) : G.order - (H.adjoin (G.chain.generators[↑i].conj H.generators[↑j])).order < G.order - H.order

def Hex.PermGroup.Normal.iterate {n : Nat} (G : Group n) (remaining : Nat) (H : Group n) (hH : H.IsSubgroup G) (bound : G.order - H.order ≤ remaining) : Closure G H

Iterate strict insertions under the proved order bound. The zero case cannot truncate an unfinished normal closure.

Equations

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

def Hex.PermGroup.Normal.close {n : Nat} (G H : Group n) (hH : H.IsSubgroup G) : Closure G H

Insert missing conjugates until a full pass adds nothing. The iteration bound follows from strict order growth and cannot produce an incomplete answer.

Equations

• Hex.PermGroup.Normal.close G H hH = Hex.PermGroup.Normal.iterate G (G.order - H.order) H hH ⋯

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

The least normal subgroup of G containing H, with complete replay data.

Equations

• G.normalClosureCert H h = Hex.PermGroup.Normal.close G H h

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

Start from the subgroup and adjoin forced conjugates until it is normal.

Equations

• G.normalClosure H h = (G.normalClosureCert H h).group

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

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

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

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

The universal property rules out extraneous elements, not merely failures of normality. The containing subgroup need only be closed under G conjugation.