def Hex.PermGroup.Series.construct {n : Nat} {budget : Execution.Budget} (terms : Nat) (G : Group n) : Execution.Run budget { result : BoundedResult G // result.certificate.terms ≤ terms }

The term cap and producer meter are independent. A term cap yields a checked prefix; exhausting producer work yields no solvability verdict.

Equations

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

def Hex.PermGroup.Group.derivedSeriesBudgeted {n : Nat} (budget : Execution.Budget) (G : Group n) (terms : Nat) : Execution.Measured budget { result : Series.BoundedResult G // result.certificate.terms ≤ terms }

Bound the complete cost of derived steps as well as the number of terms. Every successful result carries its checked-prefix and term-count contracts; only a terminal certificate yields a solvability answer.

Equations

• Hex.PermGroup.Group.derivedSeriesBudgeted budget G terms = Hex.PermGroup.Execution.run budget (Hex.PermGroup.Series.construct terms G)