Acceptance gates for bounded Turing-machine traces

This definitions layer appends one final AND gate to a complete bounded-trace fragment. Its inputs are the final configuration atoms asserting that the machine is halted and that output cell one contains 1. The appended gate is therefore both the raw circuit's designated output and the acceptance bit used when the raw circuit is reconstructed as a typed single-output circuit.

noncomputable def Complexity.CircuitUnrolling.acceptanceGate {k : ℕ} (tm : NTM k) (T configBase : ℕ) : CircuitCode.RawGate

Final AND gate testing the halted state and output-cell-one acceptance conditions in a packed configuration block.

Equations

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

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

Complete bounded trace followed by its single acceptance-output gate.

Equations

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

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

Machine-dependent coefficient absorbing the final acceptance gate into the cubic bounded-trace size bound.

Equations

• Complexity.CircuitUnrolling.acceptanceSizeCoeff tm = Complexity.CircuitUnrolling.traceSizeCoeff tm + 1

def Complexity.CircuitUnrolling.boundedAcceptanceBit {k n : ℕ} (tm : NTM k) (T : ℕ) (x : BitString n) (choices : BitString T) : Bool

Exact bounded-trace acceptance bit computed from one data input and one choice string.

Equations

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