Direct-unrolling finalization generator -- definitions

This phase emits the original acceptance gate, pads with dead constant gates until the precomputed closed frontier, and finally copies the saved acceptance wire. The binary padding driver uses available itself as its counter, so no gate-counting pass or unary work fuel is needed.

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.currentAcceptanceGate {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : CircuitCode.RawGate

Numeric acceptance gate reconstructed from the current final-configuration base and horizon.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.acceptanceReferenceValues {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : BinaryValues WorkCount

Pure endpoint of acceptance-reference preparation.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.afterAcceptanceValues {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : BinaryValues WorkCount

Pure endpoint after saving and emitting the original acceptance gate.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceStateReference {k : ℕ} (tm : TM k) : BinaryRoutine WorkCount

Prepare the final-state reference of the numeric acceptance gate.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceCellPrefix {k : ℕ} (tm : TM k) : BinaryRoutine WorkCount

Add the final output tape's cell-block base to the second reference.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceCellOffset (k : ℕ) : BinaryRoutine WorkCount

Add output-cell position one and symbol-one's fixed offset.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceReferences {k : ℕ} (tm : TM k) : BinaryRoutine WorkCount

Prepare the two absolute references of the numeric acceptance gate.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitAcceptance {k : ℕ} (tm : TM k) : BinaryRoutine WorkCount

Emit the original acceptance gate and save its absolute output wire.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPaddingGate : BinaryRoutine WorkCount

One dead constant-false padding gate. The surrounding loop, rather than this body, advances available.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPadding : BinaryRoutine WorkCount

Emit dead gates until available = frontier.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTerminalCopy : BinaryRoutine WorkCount

Emit the terminal gate that restores the original acceptance output.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization {k : ℕ} (tm : TM k) : BinaryRoutine WorkCount

Complete acceptance, padding, and terminal-copy phase.

Equations

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