structure Hex.PermGroup.Derived.Certificate (n : Nat) : Type

Replay starts from a supplied complete chain for the forced commutator array, so the checker never reruns the chain producer.

• seed : Chain n
• trace : List (Normal.Step n)

def Hex.PermGroup.Derived.check {n : Nat} (G K : Group n) (c : Certificate n) : Bool

Equations

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

theorem Hex.PermGroup.Derived.check_spec {n : Nat} {G K : Group n} {c : Certificate n} (h : check G K c = true) : SameGroup K G.derived

def Hex.PermGroup.Derived.certificate {n : Nat} (G : Group n) : Certificate n

Extract independent replay data from the deterministic producer.

Equations

• Hex.PermGroup.Derived.certificate G = { seed := (Hex.PermGroup.Derived.seedGroup G).chain, trace := G.derivedCert.trace }

theorem Hex.PermGroup.Derived.checked {n : Nat} (G : Group n) : check G G.derived (certificate G) = true

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

Keep the output group and its certificate together so callers computing a series do not rebuild the same normal closure to extract its trace.

• group : Group n
• certificate : Certificate n
• checked : check G self.group self.certificate = true

theorem Hex.PermGroup.Derived.Result.inside {n : Nat} {G : Group n} (r : Result G) : r.group.IsSubgroup G

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

Equations

• Hex.PermGroup.Derived.build G = { group := G.derivedCert.group, certificate := { seed := (Hex.PermGroup.Derived.seedGroup G).chain, trace := G.derivedCert.trace }, checked := ⋯ }