inductive Hex.PermGroup.Series.Certificate (n : Nat) : Type

Every strict derived subgroup is retained. A negative terminal certificate also retains the derived subgroup and its checked equality with its parent.

• trivial {n : Nat} : Certificate n
• perfect {n : Nat} (group : Group n) (derived : Derived.Certificate n) : Certificate n
• step {n : Nat} (group : Group n) (derived : Derived.Certificate n) (tail : Certificate n) : Certificate n

def Hex.PermGroup.Series.Certificate.accepted {n : Nat} : Certificate n → Bool

Equations

• Hex.PermGroup.Series.Certificate.trivial.accepted = true
• (Hex.PermGroup.Series.Certificate.perfect group derived).accepted = false
• (Hex.PermGroup.Series.Certificate.step group derived tail).accepted = tail.accepted

def Hex.PermGroup.Series.Certificate.orders {n : Nat} (G : Group n) : Certificate n → List Nat

Include the repeated terminal term when the series stops at a fixed point.

Equations

• Hex.PermGroup.Series.Certificate.orders G Hex.PermGroup.Series.Certificate.trivial = [G.order]
• Hex.PermGroup.Series.Certificate.orders G (Hex.PermGroup.Series.Certificate.perfect group derived) = [G.order, group.order]
• Hex.PermGroup.Series.Certificate.orders G (Hex.PermGroup.Series.Certificate.step group derived tail) = G.order :: Hex.PermGroup.Series.Certificate.orders group tail

def Hex.PermGroup.Series.Certificate.depth {n : Nat} : Certificate n → Nat

Equations

• Hex.PermGroup.Series.Certificate.trivial.depth = 0
• (Hex.PermGroup.Series.Certificate.perfect group derived).depth = 0
• (Hex.PermGroup.Series.Certificate.step group derived tail).depth = tail.depth + 1

def Hex.PermGroup.Series.Certificate.terms {n : Nat} : Certificate n → Nat

Derived constructions include the terminal perfectness test.

Equations

• Hex.PermGroup.Series.Certificate.trivial.terms = 0
• (Hex.PermGroup.Series.Certificate.perfect group derived).terms = 1
• (Hex.PermGroup.Series.Certificate.step group derived tail).terms = tail.terms + 1

def Hex.PermGroup.Series.Certificate.terminal {n : Nat} (G : Group n) : Certificate n → Group n

Equations

• Hex.PermGroup.Series.Certificate.terminal G Hex.PermGroup.Series.Certificate.trivial = G
• Hex.PermGroup.Series.Certificate.terminal G (Hex.PermGroup.Series.Certificate.perfect group derived) = G
• Hex.PermGroup.Series.Certificate.terminal G (Hex.PermGroup.Series.Certificate.step group derived tail) = Hex.PermGroup.Series.Certificate.terminal group tail

def Hex.PermGroup.Series.check {n : Nat} (G : Group n) : Certificate n → Bool

Complete series replay rejects missing derived steps, false fixed points and nontrivial groups claimed to be trivial.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Series.check G Hex.PermGroup.Series.Certificate.trivial = G.isTrivial
• Hex.PermGroup.Series.check G (Hex.PermGroup.Series.Certificate.perfect group derived) = (!G.isTrivial && Hex.PermGroup.Derived.check G group derived && group.sameGroup G)

theorem Hex.PermGroup.Series.step_equiv {n : Nat} {G H : Group n} {c : Derived.Certificate n} (h : Derived.check G H c = true) : G.IsSolvable ↔ H.IsSolvable

theorem Hex.PermGroup.Series.perfect_false {n : Nat} {G H : Group n} {c : Derived.Certificate n} (h : check G (Certificate.perfect H c) = true) : ¬G.IsSolvable

theorem Hex.PermGroup.Series.check_spec {n : Nat} {G : Group n} {c : Certificate n} (h : check G c = true) : c.accepted = true ↔ G.IsSolvable

Both positive and negative checked answers have the mathematical meaning of solvability; no exhaustion branch is interpreted as a negative answer.

theorem Hex.PermGroup.Series.check_growth {n : Nat} {G : Group n} {c : Certificate n} (h : check G c = true) : 2 ^ c.depth * (Certificate.terminal G c).order ≤ G.order

Complete replay proves the logarithmic bound on strict series steps.

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

A complete certificate, whose terminal tag determines the answer.

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

def Hex.PermGroup.Series.Result.accepted {n : Nat} {G : Group n} (r : Result G) : Bool

Equations

• r.accepted = r.certificate.accepted

theorem Hex.PermGroup.Series.Result.accepted_iff {n : Nat} {G : Group n} (r : Result G) : r.accepted = true ↔ G.IsSolvable

def Hex.PermGroup.Series.Result.trivial {n : Nat} (G : Group n) (h : G.isTrivial = true) : Result G

Equations

• Hex.PermGroup.Series.Result.trivial G h = { certificate := Hex.PermGroup.Series.Certificate.trivial, checked := h }

def Hex.PermGroup.Series.Result.perfect {n : Nat} (G : Group n) (d : Derived.Result G) (ht : G.isTrivial ≠ true) (he : d.group.sameGroup G = true) : Result G

Equations

• Hex.PermGroup.Series.Result.perfect G d ht he = { certificate := Hex.PermGroup.Series.Certificate.perfect d.group d.certificate, checked := ⋯ }

def Hex.PermGroup.Series.Result.prepend {n : Nat} (G : Group n) (d : Derived.Result G) (he : d.group.sameGroup G ≠ true) (tail : Result d.group) : Result G

Equations

• Hex.PermGroup.Series.Result.prepend G d he tail = { certificate := Hex.PermGroup.Series.Certificate.step d.group d.certificate tail.certificate, checked := ⋯ }

theorem Hex.PermGroup.Series.derived_decreases {n : Nat} (G : Group n) (d : Derived.Result G) (he : d.group.sameGroup G ≠ true) : d.group.order < G.order

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

A strict decrease at least halves the order. The proved bound cannot expire before a trivial term or a certified nontrivial fixed point.

Equations

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

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

Equations

• Hex.PermGroup.Series.build G = Hex.PermGroup.Series.iterate G.order G ⋯

def Hex.PermGroup.Group.derivedSeries {n : Nat} (G : Group n) : Series.Result G

Compute the complete derived series through its certified terminal term.

Equations

• G.derivedSeries = Hex.PermGroup.Series.build G

def Hex.PermGroup.Group.isSolvable {n : Nat} (G : Group n) : Bool

Equations

• G.isSolvable = G.derivedSeries.accepted

theorem Hex.PermGroup.Group.isSolvable_iff {n : Nat} (G : Group n) : G.isSolvable = true ↔ G.IsSolvable