Direct-unrolling packed-step generator -- definitions

One step enumerates states, heads, and cells in the explicit configuration wire order. After all next formulas have streamed, it replays the same compact enumeration using only fixed size polynomials to emit the delayed packed-output copies. gateBound temporarily saves the formula-stream base and gateCount is reused, after its header has already been emitted, as the rolling source cursor. Neither requires a new work tape.

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

Clean entry for one packed transition layer. The stronger moved-head contract contains every scratch condition needed by the other next-atom branches; position and the shared outer position limit are additionally zero at whole-step entry.

• movedHeadClean : MovedHeadFormulaClean values

  All nested next-formula scratch is reusable.

• position : values Work.position = 0

  The explicit atom-position counter starts clear.

• limit₁ : values Work.limit₁ = 0

  The explicit atom-position limit starts clear.

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepWidthEnvelope {k : ℕ} (tm : NTM k) (values : BinaryValues WorkCount) (width : ℕ) : Prop

One shared numeric envelope for every prefix of a packed transition step. The first field retains arbitrary incoming registers. The second dominates the complete output frontier together with every absolute reference and polynomial evaluator that can be live inside a nested next-formula or delayed-copy phase.

• values_le (index : Fin WorkCount) : values index ≤ width

  Every incoming register fits the common width.

• cap (state : tm.Q) (headTape : TapeSlot k) (writtenTape : WritableSlot k) (symbol : Γ) (stateIndex tapeIndex symbolIndex position : ℕ) : stateIndex < Fintype.card tm.Q → tapeIndex ≤ k + 1 → symbolIndex < 4 → position ≤ values Work.horizon + 1 → values Work.available + stepScheduleSize (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (stepAtomKindAt tm (values Work.horizon)) (stepAtomEffectSelectedAt tm (values Work.horizon)) (effectCaseChoiceAt tm) + transitionStateRef (values Work.configBase) stateIndex + (transitionHeadRef (Fintype.card tm.Q) (values Work.horizon) (values Work.configBase) tapeIndex position + tapeIndex + values Work.horizon + 1) + (transitionCellRef (Fintype.card tm.Q) (k + 2) (values Work.horizon) (values Work.configBase) tapeIndex position symbolIndex + (tapeIndex * (values Work.horizon + 2) + position) + (values Work.horizon + 2) + (k + 2) + tapeIndex + 4) + caseReadSize (values Work.horizon) + 2 * TM.binaryPolynomialValueCap predecessorHeadSchedulePolynomial (values Work.horizon) + 2 * (values Work.horizon + 2) + values Work.horizon + 2 * TM.binaryPolynomialValueCap (stateNextChildPolynomial tm state) (values Work.horizon) + 2 * TM.binaryPolynomialValueCap (headNextChildPolynomial tm headTape) (values Work.horizon) + 2 * TM.binaryPolynomialValueCap (writtenNextChildPolynomial tm writtenTape symbol) (values Work.horizon) + 2 * TM.binaryPolynomialValueCap (stateNextFormulaPolynomial tm state) (values Work.horizon) + 2 * TM.binaryPolynomialValueCap (headNextFormulaPolynomial tm headTape) (values Work.horizon) + 2 * TM.binaryPolynomialValueCap (writtenNextFormulaPolynomial tm writtenTape symbol) (values Work.horizon) + 2 * TM.binaryPolynomialValueCap (Polynomial.C 1) (values Work.horizon) ≤ width

  The complete step frontier and every nested arithmetic quantity fit simultaneously.

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.setStepPositionLimit (extra : ℕ) : BinaryRoutine WorkCount

Replace the outer position limit by horizon + extra.

Equations

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

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

Emit all fixed state-atom next formulas.

Equations

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

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

Emit the remaining head-position formulas for one fixed named tape, starting at the current position and stopping at the shared limit.

Equations

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

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

Emit the four immutable cell formulas at the current position.

Equations

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

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

Emit the four writable-cell formulas at the current position, using the immutable marker schedule exactly at position zero.

Equations

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

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

Emit the remaining cell-position formulas for one fixed named tape, starting at the current position and stopping at the shared limit.

Equations

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

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

Emit the complete forward next-formula stream in canonical atom order.

Equations

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

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

Emit all delayed state-formula output copies.

Equations

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

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

Emit the remaining delayed head-formula output copies for one fixed tape, starting at the current position and stopping at the shared limit.

Equations

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

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

Emit four one-gate immutable-cell output copies at the current position.

Equations

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

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

Emit four writable-cell output copies at the current position.

Equations

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

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

Replay the remaining cell enumeration to emit delayed copies for one tape, starting at the current position and stopping at the shared limit.

Equations

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

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

Emit the complete delayed packed-copy suffix in canonical atom order.

Equations

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

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

Emit one complete packed transition layer. On exit configBase is the first wire of the packed successor configuration.

Equations

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