Direct-unrolling written-cell generator -- definitions

The run-time cell position is parked while the nested selected-write effect reuses the read-formula counters. The first head-at-cell output is retained in one enclosing register; the remaining six gates then stream with only recent references. The final represented cell has no head wire, detected by a bounded subtraction from horizon + 1 rather than a general equality routine.

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.HeadAtCurrentCellClean (values : BinaryValues WorkCount) : Prop

Scratch contract for one numeric head-at-current-cell test. The cell position and tape selector are inputs and are deliberately preserved.

• loop₃ : values Work.loop₃ = 0

  The bounded subtraction controller starts clear.

• temporary₃ : values Work.temporary₃ = 0

  The horizon-gap temporary starts clear.

• reference₀ : values Work.reference₀ = 0

  The canonical constant-gate reference starts clear.

• emitCounter : values Work.emitCounter = 0

  The raw-gate emission counter is reusable.

• copyCounter : values Work.copyCounter = 0

  The framed-copy counter is reusable.

• multiplyCounter : values Work.multiplyCounter = 0

  The framed-multiplication counter is reusable.

• addCounter : values Work.addCounter = 0

  The framed-addition counter is reusable.

• temporary₀ : values Work.temporary₀ = 0

  The head-reference arithmetic temporary starts clear.

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.WrittenCellFormulaClean (values : BinaryValues WorkCount) : Prop

Clean writable-cell entry, allowing position itself to hold the positive cell position while every nested case scratch register is otherwise clear.

• caseClean : CaseFormulaClean (Function.update values Work.position 0)

  Nested case emission is clean after parking the cell position.

• limit₂ : values Work.limit₂ = 0

  Position-save register starts clear.

• savedOutput : values Work.savedOutput = 0

  First head-test output save register starts clear.

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCellGate (stateCount : ℕ) : BinaryRoutine WorkCount

Emit the final head-at-cell gate from a prepared horizon gap. A zero gap means that the current cell has no represented old-head wire.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCell (stateCount : ℕ) : BinaryRoutine WorkCount

Emit the numeric head-at-cell gate at the current tape and cell position. The final cell horizon + 1 emits false; every earlier cell copies its head wire.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellEffect {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) : BinaryRoutine WorkCount

Emit the transition effect selected by a fixed writable tape and symbol.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) : BinaryRoutine WorkCount

Emit the complete positive writable-cell formula for fixed tape/symbol data and the run-time position in Work.position.

Equations

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