Structure of bounded-trace acceptance circuits

This internal module proves that appending the final halt-and-output test adds exactly one gate, preserves topological well-formedness, and retains a cubic machine-dependent size bound.

theorem Complexity.CircuitUnrolling.acceptanceGate_wellFormedAt_internal {k : ℕ} (tm : NTM k) (T configBase available : ℕ) (hconfig : configBase + configWidth tm T ≤ available) : (acceptanceGate tm T configBase).WellFormedAt available

A final acceptance gate is well formed whenever its packed configuration block lies in the existing wire prefix.

theorem Complexity.CircuitUnrolling.finalAcceptanceGate_wellFormedAt_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : (acceptanceGate tm T (traceOutputBase tm T n available layout)).WellFormedAt (available + traceFragmentSize tm T n available layout)

The canonical final acceptance gate points only into the final packed configuration block at the end of the trace fragment.

theorem Complexity.CircuitUnrolling.length_acceptanceRawCircuit_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : List.length (acceptanceRawCircuit tm T n available layout) = traceFragmentSize tm T n available layout + 1

Appending the final test adds exactly one gate to the complete trace.

theorem Complexity.CircuitUnrolling.acceptanceRawCircuit_topologicallyWellFormed_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (acceptanceRawCircuit tm T n available layout)

The complete trace plus its final acceptance gate is topologically ordered after the primary-wire prefix.

theorem Complexity.CircuitUnrolling.acceptanceRawCircuit_wellFormed_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) : CircuitCode.RawCircuit.WellFormed available (acceptanceRawCircuit tm T n available layout)

The appended acceptance gate makes the raw circuit nonempty, so topology upgrades directly to full raw-circuit well-formedness.

theorem Complexity.CircuitUnrolling.length_acceptanceRawCircuit_le_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : List.length (acceptanceRawCircuit tm T n available layout) ≤ acceptanceSizeCoeff tm * (T + 2) ^ 3

The final acceptance gate is absorbed into a machine-dependent cubic gate-count bound.