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

An untrusted normal-closure insertion names an ambient symmetric generator, a current subgroup generator, and the complete chain after adjoining their conjugate. The next generator array is reconstructed by the checker.

• conjugator : Nat
• source : Nat
• chain : Chain n

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

Check a strict, forced conjugate insertion. Arbitrary extra generators cannot enter through the supplied chain.

Equations

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

theorem Hex.PermGroup.Normal.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), ∃ (j : Fin H.generators.size), SameGroup K (H.adjoin (G.chain.generators[↑i].conj H.generators[↑j])) ∧ ¬Generated H.generators (G.chain.generators[↑i].conj H.generators[↑j])

theorem Hex.PermGroup.Normal.step_adjoin {n : Nat} (G H : Group n) (i : Fin G.chain.generators.size) (j : Fin H.generators.size) (h : ¬Generated H.generators (G.chain.generators[↑i].conj H.generators[↑j])) : have p := G.chain.generators[↑i].conj H.generators[↑j]; step G H { conjugator := ↑i, source := ↑j, chain := (H.adjoin p).chain } = some (H.adjoin p)

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

theorem Hex.PermGroup.Normal.step_least {n : Nat} {G H K N : Group n} {s : Step n} (h : step G H s = some K) (hH : H.IsSubgroup N) (hN : check G N = true) : K.IsSubgroup N

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

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

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

Replay each complete chain and forced conjugate, preserving the exact generator order at every stage.

Equations

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

theorem Hex.PermGroup.Normal.replay_least {n : Nat} {G H K N : Group n} {trace : List (Step n)} (h : replay G H trace = some K) (hH : H.IsSubgroup N) (hN : check G N = true) : K.IsSubgroup N

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

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

theorem Hex.PermGroup.Normal.replay_lift {n : Nat} {G H K : Group n} {trace : List (Step n)} {P : Perm n → Prop} (h : replay G H trace = some K) (hid : P (Perm.id n)) (hmul : ∀ (p q : Perm n), P p → P q → P (p.comp q)) (hinv : ∀ (p : Perm n), P p → P p.inv) (hconj : ∀ (g p : Perm n), Generated G.generators g → P p → P (g.conj p)) (hH : ∀ (p : Perm n), Generated H.generators p → P p) (p : Perm n) : Generated K.generators p → P p

Every replayed element belongs to any subgroup predicate containing the input and closed under ambient conjugation. This also applies to subgroups that have no computational generator presentation.

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

The replay trace grows by a factor of at least two at each step.