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

A bounded run either has a complete terminal certificate or retains a checked prefix ending at a pending group. Pending does not mean nonsolvable.

• pending {n : Nat} : Partial n
• complete {n : Nat} (certificate : Certificate n) : Partial n
• step {n : Nat} (group : Group n) (derived : Derived.Certificate n) (tail : Partial n) : Partial n

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

Equations

• Hex.PermGroup.Series.Partial.check G Hex.PermGroup.Series.Partial.pending = !G.isTrivial
• Hex.PermGroup.Series.Partial.check G (Hex.PermGroup.Series.Partial.complete c) = Hex.PermGroup.Series.check G c
• Hex.PermGroup.Series.Partial.check G (Hex.PermGroup.Series.Partial.step H c tail) = (Hex.PermGroup.Derived.check G H c && !H.sameGroup G && Hex.PermGroup.Series.Partial.check H tail)

def Hex.PermGroup.Series.Partial.complete? {n : Nat} : Partial n → Option (Certificate n)

Equations

• Hex.PermGroup.Series.Partial.pending.complete? = none
• (Hex.PermGroup.Series.Partial.complete c).complete? = some c
• (Hex.PermGroup.Series.Partial.step H c tail).complete? = Option.map (Hex.PermGroup.Series.Certificate.step H c) tail.complete?

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

Equations

• Hex.PermGroup.Series.Partial.pending.terms = 0
• (Hex.PermGroup.Series.Partial.complete c).terms = c.terms
• (Hex.PermGroup.Series.Partial.step H c tail).terms = tail.terms + 1

theorem Hex.PermGroup.Series.Partial.complete_checked {n : Nat} {G : Group n} {p : Partial n} {c : Certificate n} (h : check G p = true) (hc : p.complete? = some c) : Series.check G c = true

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

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

def Hex.PermGroup.Series.BoundedResult.answer? {n : Nat} {G : Group n} (r : BoundedResult G) : Option Bool

none means the checked prefix has not reached a terminal group.

Equations

• r.answer? = Option.map Hex.PermGroup.Series.Certificate.accepted r.certificate.complete?

theorem Hex.PermGroup.Series.BoundedResult.answer_spec {n : Nat} {G : Group n} (r : BoundedResult G) {b : Bool} (h : r.answer? = some b) : b = true ↔ G.IsSolvable

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

Equations

• Hex.PermGroup.Series.BoundedResult.ofResult r = { certificate := Hex.PermGroup.Series.Partial.complete r.certificate, checked := ⋯ }

def Hex.PermGroup.Series.BoundedResult.pending {n : Nat} (G : Group n) (h : G.isTrivial ≠ true) : BoundedResult G

Equations

• Hex.PermGroup.Series.BoundedResult.pending G h = { certificate := Hex.PermGroup.Series.Partial.pending, checked := ⋯ }

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

Equations

• Hex.PermGroup.Series.BoundedResult.prepend G d h tail = { certificate := Hex.PermGroup.Series.Partial.step d.group d.certificate tail.certificate, checked := ⋯ }

def Hex.PermGroup.Series.bounded {n : Nat} (terms : Nat) (G : Group n) : BoundedResult G

The cap counts derived-subgroup constructions, including the terminal fixed-point check. It is checked before the next commutator array is built.

Equations

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

theorem Hex.PermGroup.Series.bounded_terms {n : Nat} (terms : Nat) (G : Group n) : (bounded terms G).certificate.terms ≤ terms

def Hex.PermGroup.Group.derivedSeriesCapped {n : Nat} (G : Group n) (terms : Nat) : Series.BoundedResult G

A bounded derived series preserves its complete checked prefix on exhaustion; only terminal certificates produce a Boolean solvability answer.

Equations

• G.derivedSeriesCapped terms = Hex.PermGroup.Series.bounded terms G