Delayed packed-formula copies -- definitions

The direct step generator emits every successor formula before its packed output block. gateCount is a rolling cursor through those formula blocks. This primitive advances that cursor by a fixed polynomial in the tableau horizon and copies the final wire of the newly traversed block.

The explicit domain requires the formula-size polynomial to be positive. That deliberately rules out empty formula blocks independently of the old cursor value.

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPackedFormulaCopy (sizePolynomial : Polynomial ℕ) : BinaryRoutine WorkCount

Advance the rolling formula cursor by sizePolynomial(horizon) and emit a copy of the newly traversed formula block's output wire.

Equations

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