def Hex.PermGroup.Derived.construct {n : Nat} {budget : Execution.Budget} (G : Group n) : Execution.Run budget (Result G)

A derived step reserves its commutator array before materialization, then threads the same meter through the seed chain and every normal-closure rebuild.

Equations

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

def Hex.PermGroup.Group.derivedBudgeted {n : Nat} (budget : Execution.Budget) (G : Group n) : Execution.Measured budget (Derived.Result G)

Exhaustion of a derived step returns no final derived subgroup. Its seed construction and normal closure consume a single cumulative producer meter.

Equations

• Hex.PermGroup.Group.derivedBudgeted budget G = Hex.PermGroup.Execution.run budget (Hex.PermGroup.Derived.construct G)