Direct-unrolling moved-head generator -- definitions

The three fixed direction members are emitted in left/right/stay order. The run-time target position is saved while nested effect formulas reuse the position register. Each completed member output is retained in one otherwise unused enclosing register, so the final three-way disjunction needs no dynamic size recomputation.

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

Clean moved-head entry. Updating position to zero exposes exactly the case-formula scratch convention required by each nested effect formula.

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

  Nested case emission is clean once the target position is parked.

• limit₂ : values Work.limit₂ = 0

  Target-position save register starts clear.

• loop₁ : values Work.loop₁ = 0

  The predecessor connector-loop counter starts clear.

• savedOutput : values Work.savedOutput = 0

  First direction-output save register starts clear.

• direction : values Work.direction = 0

  Second direction-output save register starts clear.

• atomKind : values Work.atomKind = 0

  Third direction-output save register starts clear.

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadEffect {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) : BinaryRoutine WorkCount

Emit the selected transition effect for one fixed movement direction.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadConjunction : BinaryRoutine WorkCount

Combine the selected-effect output with the predecessor-head output. The effect output is predecessorSize + 1 wires behind the current frontier.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.saveMovedHeadMemberOutput (save : Fin WorkCount) : BinaryRoutine WorkCount

Preserve the immediately preceding member output in a fixed enclosing register without emitting any code bits.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.saveMovedHeadMemberOutput save = Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareRecentReference save 1

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadMember {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) (directionCode : ℕ) (save : Fin WorkCount) : BinaryRoutine WorkCount

Emit one direction member, restore the nested case scratch convention, and retain its conjunction output in save.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitSavedMovedHeadConnector (save : Fin WorkCount) : BinaryRoutine WorkCount

Emit one disjunction connector from a saved member output and the immediately preceding identity or connector.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : BinaryRoutine WorkCount

Emit the complete left/right/stay moved-head formula and restore the original target position.

Equations

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