Direct-unrolling next-atom generator -- definitions

State, head, and positive writable-cell atoms share one executable halted-or wrapper. Its two long-distance references are recovered by evaluating the fixed child-size polynomial after child emission. Immutable input cells and writable marker cells use a direct old-cell copy.

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

Scratch registers owned by the fixed halted-or wrapper. The old-value and child routines may impose additional branch-specific cleanliness contracts.

• reference₀ : values Work.reference₀ = 0

  First raw-gate reference starts clear.

• reference₁ : values Work.reference₁ = 0

  Second raw-gate reference starts clear.

• emitCounter : values Work.emitCounter = 0

  Raw-gate emission counter is reusable.

• copyCounter : values Work.copyCounter = 0

  Framed-copy counter is reusable.

• multiplyCounter : values Work.multiplyCounter = 0

  Polynomial multiplication counter is reusable.

• addCounter : values Work.addCounter = 0

  Polynomial addition counter is reusable.

• loop₃ : values Work.loop₃ = 0

  Dynamic-offset predecessor counter starts clear.

• temporary₃ : values Work.temporary₃ = 0

  Evaluated dynamic offset starts clear.

• polynomialScratch : values Work.polynomialScratch = 0

  Polynomial evaluation accumulator starts clear.

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHaltedOrFormula (haltStateIndex : ℕ) (childSize : Polynomial ℕ) (oldValue nextValue : BinaryRoutine WorkCount) : BinaryRoutine WorkCount

Fixed halted-or wrapper around a one-gate old-value routine and a nested next-value routine with a known horizon-size polynomial.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldStateValue (stateIndex : ℕ) : BinaryRoutine WorkCount

Emit a state atom's old-value copy.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldStateValue stateIndex = Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStateReference stateIndex

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

Emit a head atom's old-value copy while preserving its run-time target position.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitOldCellValue (stateCount tapeCount tapeIndex symbolIndex : ℕ) : BinaryRoutine WorkCount

Emit a cell atom's old-value copy while preserving its run-time position.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.stateNextChildPolynomial {k : ℕ} (tm : NTM k) (state : tm.Q) : Polynomial ℕ

Fixed selected-effect size polynomial for one state atom.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.stateNextFormulaPolynomial {k : ℕ} (tm : NTM k) (state : tm.Q) : Polynomial ℕ

Complete halted-or state-formula size polynomial.

Equations

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

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

Fixed selected-effect routine for one state atom.

Equations

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

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

Emit a complete state-atom next formula.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextChildPolynomial {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : Polynomial ℕ

Fixed moved-head size polynomial for one named tape.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextFormulaPolynomial {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : Polynomial ℕ

Complete halted-or head-formula size polynomial.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextFormulaPolynomial tm tape = Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextChildPolynomial tm tape + Polynomial.C 7

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

Emit a complete head-atom next formula at the run-time target position.

Equations

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

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

Fixed written-cell size polynomial for one writable tape and symbol.

Equations

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

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

Complete halted-or positive writable-cell size polynomial.

Equations

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

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

Emit a complete positive writable-cell next formula at the run-time position.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy (stateCount tapeCount tapeIndex symbolIndex : ℕ) : BinaryRoutine WorkCount

Emit one immutable input or writable marker-cell old-value copy.

Equations

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