Definitions for tiled bounded-trace circuits

This definitions layer concatenates the initial-configuration fragment with one packed transition fragment for every bounded choice. Every transition is compiled at the original horizon T, reads the preceding packed configuration block, and uses its corresponding primary choice wire.

The intermediate TraceBuild record exposes the current packed block and the first unused wire. This makes the recursive layout available to later proofs of topology, evaluation, and polynomial size without introducing dependent casts into the circuit construction itself.

structure Complexity.CircuitUnrolling.TraceBuild : Type

Accumulated circuit data while tiling a bounded machine trace.

• circuit : CircuitCode.RawCircuit

  All initialization and transition gates emitted so far.

• configBase : ℕ

  First wire of the most recently packed configuration block.

• available : ℕ

  First unused absolute wire after the accumulated circuit.

• size : ℕ

  Exact number of gates emitted after the original primary-wire prefix.

noncomputable def Complexity.CircuitUnrolling.initialTraceBuild {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : TraceBuild

Initialize a trace build after available primary wires.

Arguments after the machine are the horizon, input length, primary-wire count, and the locations of choices and input data in that primary prefix.

Equations

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

noncomputable def Complexity.CircuitUnrolling.traceBuildStep {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} (layout : InputWires T n primaryAvailable) (build : TraceBuild) (i : Fin T) : TraceBuild

Append the transition selected by choice index i to an accumulated build.

The horizon remains the original T; only the incoming configuration base and the first unused wire advance from one layer to the next.

Equations

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

noncomputable def Complexity.CircuitUnrolling.traceBuildFrom {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} (layout : InputWires T n primaryAvailable) (build : TraceBuild) (indices : List (Fin T)) : TraceBuild

Append a listed sequence of bounded transition layers to an existing build.

Indices are consumed from left to right. The list interface supports induction over partial traces while keeping every index in the fixed type Fin T.

Equations

• Complexity.CircuitUnrolling.traceBuildFrom tm layout build indices = List.foldl (Complexity.CircuitUnrolling.traceBuildStep tm layout) build indices

noncomputable def Complexity.CircuitUnrolling.prefixTraceBuild {k : ℕ} (tm : NTM k) (T n available i : ℕ) (layout : InputWires T n available) : TraceBuild

Partial trace build containing the first i canonical choice indices. When i ≥ T, list take saturates and this is the complete build.

Equations

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

noncomputable def Complexity.CircuitUnrolling.traceBuild {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : TraceBuild

Complete bounded-trace build: initialization followed by choices 0, ..., T - 1 in order. At horizon zero this is just initialization.

Equations

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

noncomputable def Complexity.CircuitUnrolling.traceFragment {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : CircuitCode.RawCircuit

Raw circuit for the complete bounded trace.

Equations

• Complexity.CircuitUnrolling.traceFragment tm T n available layout = (Complexity.CircuitUnrolling.traceBuild tm T n available layout).circuit

noncomputable def Complexity.CircuitUnrolling.traceOutputBase {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : ℕ

First wire of the final packed configuration block.

Equations

• Complexity.CircuitUnrolling.traceOutputBase tm T n available layout = (Complexity.CircuitUnrolling.traceBuild tm T n available layout).configBase

noncomputable def Complexity.CircuitUnrolling.traceFragmentSize {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : ℕ

Exact recursively accumulated gate count of the complete trace fragment.

Equations

• Complexity.CircuitUnrolling.traceFragmentSize tm T n available layout = (Complexity.CircuitUnrolling.traceBuild tm T n available layout).size

noncomputable def Complexity.CircuitUnrolling.traceSizeCoeff {k : ℕ} (tm : NTM k) : ℕ

Machine-dependent coefficient in the cubic bounded-trace size bound.

Equations

• Complexity.CircuitUnrolling.traceSizeCoeff tm = Complexity.CircuitUnrolling.stepSizeCoeff tm + Fintype.card tm.Q + 5 * (k + 2)