Acceptance circuits for bounded Turing-machine traces

This module appends the actual acceptance bit to a bounded trace: one final AND gate tests that the machine is halted and that output cell one contains 1. The raw circuit is topologically well formed, has cubic size, and reconstructs to a typed fan-in-two circuit whose output is exactly the predicate counted by NTM.acceptCount.

The canonical constructor places choice bits before input-data bits. Its input arity must be positive; circuit families continue to handle the unique zero-length case separately.

Main results

• acceptanceRawCircuit_wellFormed: the raw circuit is valid.
• eval?_acceptanceRawCircuit: raw evaluation returns the acceptance bit.
• acceptanceCircuit_eval: typed evaluation has the same semantics.
• canonicalAcceptanceCircuit_eval: canonical choices-first semantics.
• canonicalAcceptanceCircuit_size_le: canonical cubic size bound.
• card_acceptingChoices_eq_acceptCount: circuit acceptance counts machine accepting paths exactly.

@[simp]

theorem Complexity.CircuitUnrolling.length_acceptanceRawCircuit {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 acceptance test adds exactly one gate.

theorem Complexity.CircuitUnrolling.acceptanceRawCircuit_topologicallyWellFormed {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 raw acceptance circuit is topologically ordered after any nonempty primary-input prefix.

theorem Complexity.CircuitUnrolling.acceptanceRawCircuit_wellFormed {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 raw acceptance circuit is nonempty and topologically well formed.

theorem Complexity.CircuitUnrolling.length_acceptanceRawCircuit_le {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 raw acceptance circuit retains the trace compiler's cubic size bound.

theorem Complexity.CircuitUnrolling.evalAux?_acceptanceRawCircuit {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) (x : BitString n) (choices : Fin T → Bool) (wires : Array Bool) (hsize : wires.size = available) (hdata : ∀ (j : Fin n), wires[↑(layout.data j)]? = some (x j)) (hchoices : ∀ (j : Fin T), wires[↑(layout.choice j)]? = some (choices j)) : ∃ (traceResult : Array Bool), (acceptanceRawCircuit tm T n available layout).evalAux? wires = some (traceResult.push (decide ((tm.trace T choices (tm.initCfg x.toList)).state = tm.qhalt ∧ (tm.trace T choices (tm.initCfg x.toList)).output.cells 1 = Γ.one))) ∧ traceResult.size = wires.size + traceFragmentSize tm T n available layout ∧ (∀ i < wires.size, traceResult[i]? = wires[i]?) ∧ EncodesConfig tm T (traceOutputBase tm T n available layout) traceResult (tm.trace T choices (tm.initCfg x.toList))

Evaluating the raw acceptance circuit appends the final acceptance bit to the successfully evaluated trace array.

theorem Complexity.CircuitUnrolling.eval?_acceptanceRawCircuit {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) (x : BitString n) (choices : Fin T → Bool) (input : BitString available) (hdata : ∀ (j : Fin n), input (layout.data j) = x j) (hchoices : ∀ (j : Fin T), input (layout.choice j) = choices j) : (acceptanceRawCircuit tm T n available layout).eval? input.toList = some (decide ((tm.trace T choices (tm.initCfg x.toList)).state = tm.qhalt ∧ (tm.trace T choices (tm.initCfg x.toList)).output.cells 1 = Γ.one))

Raw single-output evaluation returns exactly the bounded-trace acceptance predicate.

noncomputable def Complexity.CircuitUnrolling.acceptanceCircuit {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) : Circuit Basis.andOr2 available 1 (List.length (acceptanceRawCircuit tm T n available layout) - 1)

Reconstruct the valid raw acceptance code as a typed fan-in-two circuit. The final raw gate becomes the sole typed output gate.

Equations

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

@[simp]

theorem Complexity.CircuitUnrolling.acceptanceCircuit_size {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) : (acceptanceCircuit tm T n available layout).size = traceFragmentSize tm T n available layout + 1

Typed reconstruction preserves the exact raw gate count.

theorem Complexity.CircuitUnrolling.acceptanceCircuit_size_le {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) : (acceptanceCircuit tm T n available layout).size ≤ acceptanceSizeCoeff tm * (T + 2) ^ 3

The typed acceptance circuit has the same machine-dependent cubic size bound as its raw representation.

theorem Complexity.CircuitUnrolling.acceptanceCircuit_eval {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) (x : BitString n) (choices : Fin T → Bool) (input : BitString available) (hdata : ∀ (j : Fin n), input (layout.data j) = x j) (hchoices : ∀ (j : Fin T), input (layout.choice j) = choices j) : (acceptanceCircuit tm T n available layout).eval input 0 = decide ((tm.trace T choices (tm.initCfg x.toList)).state = tm.qhalt ∧ (tm.trace T choices (tm.initCfg x.toList)).output.cells 1 = Γ.one)

The typed acceptance circuit computes the exact halt-and-output predicate of the bounded machine trace represented by its primary inputs.

noncomputable def Complexity.CircuitUnrolling.canonicalAcceptanceCircuit {k : ℕ} (tm : NTM k) (T n : ℕ) [NeZero (T + n)] : Circuit Basis.andOr2 (T + n) 1 (List.length (acceptanceRawCircuit tm T n (T + n) (prefixInputWires T n)) - 1)

Canonical choices-first, data-second acceptance circuit.

Equations

• Complexity.CircuitUnrolling.canonicalAcceptanceCircuit tm T n = Complexity.CircuitUnrolling.acceptanceCircuit tm T n (T + n) (Complexity.CircuitUnrolling.prefixInputWires T n)

theorem Complexity.CircuitUnrolling.canonicalAcceptanceCircuit_eval {k : ℕ} (tm : NTM k) (T n : ℕ) [NeZero (T + n)] (choices : BitString T) (x : BitString n) : (canonicalAcceptanceCircuit tm T n).eval (Fin.append choices x) 0 = decide ((tm.trace T choices (tm.initCfg x.toList)).state = tm.qhalt ∧ (tm.trace T choices (tm.initCfg x.toList)).output.cells 1 = Γ.one)

Under the canonical layout, evaluating on choices ++ x returns the machine's bounded-trace acceptance bit.

theorem Complexity.CircuitUnrolling.canonicalAcceptanceCircuit_size_le {k : ℕ} (tm : NTM k) (T n : ℕ) [NeZero (T + n)] : (canonicalAcceptanceCircuit tm T n).size ≤ acceptanceSizeCoeff tm * (T + 2) ^ 3

The canonical choices-first acceptance circuit inherits the generic cubic size bound.

theorem Complexity.CircuitUnrolling.card_acceptingChoices_eq_acceptCount {k : ℕ} (tm : NTM k) (T n : ℕ) [NeZero (T + n)] (x : BitString n) : {choices : BitString T | (canonicalAcceptanceCircuit tm T n).eval (Fin.append choices x) 0 = true}.card = tm.acceptCount x.toList T

The number of canonical choice strings accepted by the circuit is exactly the machine's bounded accepting-path count.