Direct-unrolling initialization generator -- definitions

This module assembles the first positive tableau layer from proof-carrying binary routines. Fixed machine state and tape multiplicities are unrolled at definition time; input-dependent head and cell ranges use canonical binary loops over natural counters.

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitConstantGate (value : Bool) : BinaryRoutine WorkCount

Emit one raw constant gate and advance the first-unused-wire counter.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCopyGate (reference : Fin WorkCount) (negated : Bool := false) : BinaryRoutine WorkCount

Emit one possibly negated copy gate and advance the wire counter.

Equations

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

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

Emit the four symbol gates of a left-marker cell.

Equations

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

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

Emit the four symbol gates of a blank cell.

Equations

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

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

Emit one input data cell, using loop₀ as its primary-input wire.

Equations

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

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

Emit the fixed initial-state one-hot segment.

Equations

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

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

Replace limit₀ by the current horizon plus one.

Equations

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

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

Replace limit₀ by the input length.

Equations

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

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

Emit one initial head-position bit from the current position counter.

Equations

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

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

Emit all T + 1 head-position gates for one named tape and restore the position counter to zero.

Equations

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

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

Emit the complete input-cell segment once limit₀ = T + 1.

Equations

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

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

Emit one blank writable tape's marker and T + 1 blank cells, restoring the position counter to zero.

Equations

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

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

Emit the complete positive-input initialization raw-gate stream. The entry contract is discharged later from preambleValues; on exit both loop controller tapes are restored to zero for transition serialization.

Equations

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