Complete direct-unrolling generator -- definitions

The positive tableau body emits the initial packed configuration, exactly one packed transition layer per horizon step, and the padded terminal acceptance fragment. The outer step counter is restored after the loop. Prefixing this body with program also handles the separately tagged length-zero family member.

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

Emit all packed transition layers and restore the outer step counter.

Equations

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

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.TransitionEntry {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : Prop

Compact semantic entry contract for the complete transition-layer loop.

• clean : StepClean values

  All reusable transition scratch starts clean.

• loop₂ : values Work.loop₂ = 0

  Layer enumeration starts at zero.

• horizon : 0 < values Work.horizon

  At least one represented configuration layer exists.

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

Transition-layer loop with its compact semantic precondition exposed without changing the concrete machine or any behavioral/resource field.

Equations

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

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

Compact semantic entry contract for final acceptance, padding, and copy.

• emitCounter : values Work.emitCounter = 0

  Raw-gate emission scratch is clear.

• copyCounter : values Work.copyCounter = 0

  Binary-copy scratch is clear.

• addCounter : values Work.addCounter = 0

  Addition scratch is clear.

• multiplyCounter : values Work.multiplyCounter = 0

  Multiplication scratch is clear.

• available : values Work.available + 1 ≤ values Work.frontier

  The acceptance gate fits before the closed padding frontier.

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

Finalization phase with its compact semantic precondition exposed without changing the concrete machine or any behavioral/resource field.

Equations

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

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

Complete positive-length tableau body, excluding the tagged header.

Equations

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

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

Complete zero/positive generator for the padded direct-unrolling code.

Equations

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