def Hex.PermGroup.Normal.probe {n : Nat} {budget : Execution.Budget} (G H : Group n) : Build.Computation budget (failure? G H)

Reserve a complete conjugation pass before evaluating it. Short-circuiting may use less than the reservation; it never performs an uncharged sift.

Equations

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

@[irreducible]

def Hex.PermGroup.Normal.iterateBudgeted {n : Nat} {budget : Execution.Budget} (G : Group n) (remaining : Nat) (H : Group n) (hH : H.IsSubgroup G) (bound : G.order - H.order ≤ remaining) : Execution.Run budget (Closure G H)

Every completed iteration retains its ordinary normal-closure certificate. An exhausted pass or chain construction exposes no terminal normality claim.

Equations

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

def Hex.PermGroup.Group.normalClosureBudgeted {n : Nat} (budget : Execution.Budget) (G H : Group n) (hH : H.IsSubgroup G) : Execution.Measured budget (Normal.Closure G H)

Bounded normal closure returns either a fully checked closure certificate or an explicit exhausted resource. All conjugations and nested suffix rebuilds consume one producer meter.

Equations

• Hex.PermGroup.Group.normalClosureBudgeted budget G H hH = Hex.PermGroup.Execution.run budget (Hex.PermGroup.Normal.iterateBudgeted G (G.order - H.order) H hH ⋯)