def Hex.PermGroup.Core.Member {n : Nat} (G H : Group n) (p : Perm n) : Prop

Membership in every ambient conjugate of the input subgroup.

Equations

• Hex.PermGroup.Core.Member G H p = ∀ (g : Hex.Perm n), Hex.PermGroup.Generated G.generators g → Hex.PermGroup.Generated H.generators (g.conj p)

theorem Hex.PermGroup.Core.Member.inside {n : Nat} {G H : Group n} {p : Perm n} (h : Member G H p) : Generated H.generators p

theorem Hex.PermGroup.Core.Member.conj {n : Nat} {G H : Group n} {p g : Perm n} (h : Member G H p) (hg : Generated G.generators g) : Member G H (g.conj p)

structure Hex.PermGroup.Core.Step (n : Nat) : Type

A proposed strict intersection, with a checked group and a complete search certificate. The conjugate is reconstructed from the ambient generator index.

• conjugator : Nat
• conjugate : Chain n
• group : Group n
• certificate : Search.Certificate Unit

def Hex.PermGroup.Core.step {n : Nat} (G H : Group n) (s : Step n) : Option (Group n)

Use inverse conjugation so that a failed normality test immediately witnesses strict containment. Ambient chain generators are symmetric.

Equations

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

theorem Hex.PermGroup.Core.step_spec {n : Nat} {G H K : Group n} {s : Step n} (h : step G H s = some K) : ∃ (i : Fin G.chain.generators.size), (∀ (p : Perm n), Generated K.generators p ↔ Generated H.generators p ∧ Generated H.generators (G.chain.generators[↑i].conj p)) ∧ ¬SameGroup K H

theorem Hex.PermGroup.Core.step_inside {n : Nat} {G H K : Group n} {s : Step n} (h : step G H s = some K) : K.IsSubgroup H

theorem Hex.PermGroup.Core.step_retains {n : Nat} {G H K : Group n} {s : Step n} {P : Perm n → Prop} (h : step G H s = some K) (hH : ∀ (p : Perm n), P p → Generated H.generators p) (hc : ∀ (g p : Perm n), Generated G.generators g → P p → P (g.conj p)) (p : Perm n) : P p → Generated K.generators p

theorem Hex.PermGroup.Core.step_double {n : Nat} {G H K : Group n} {s : Step n} (h : step G H s = some K) : 2 * K.order ≤ H.order

def Hex.PermGroup.Core.replay {n : Nat} (G H : Group n) : List (Step n) → Option (Group n)

Equations

• Hex.PermGroup.Core.replay G H [] = some H
• Hex.PermGroup.Core.replay G H (s :: rest) = (Hex.PermGroup.Core.step G H s).bind fun (K : Hex.PermGroup.Group n) => Hex.PermGroup.Core.replay G K rest

theorem Hex.PermGroup.Core.replay_inside {n : Nat} {G H K : Group n} {trace : List (Step n)} (h : replay G H trace = some K) : K.IsSubgroup H

theorem Hex.PermGroup.Core.replay_retains {n : Nat} {G H K : Group n} {trace : List (Step n)} {P : Perm n → Prop} (h : replay G H trace = some K) (hH : ∀ (p : Perm n), P p → Generated H.generators p) (hc : ∀ (g p : Perm n), Generated G.generators g → P p → P (g.conj p)) (p : Perm n) : P p → Generated K.generators p

theorem Hex.PermGroup.Core.replay_growth {n : Nat} {G H K : Group n} {trace : List (Step n)} (h : replay G H trace = some K) : 2 ^ trace.length * K.order ≤ H.order

Each strict intersection at least halves the group order.