Evaluation internals for parallel amplification circuits

This module evaluates the canonical prefixes of the independent-copy builder. Every completed copy records its bounded acceptance bit at the corresponding verdict wire, while later fragments preserve both the primary input prefix and all earlier verdicts. The complete copy bank then feeds those bits directly to the unary threshold compiler.

The final result intentionally remains in the dependency-light form Fin.countP: its interpretation as a block-event majority belongs above the circuit layer.

theorem Complexity.CircuitUnrolling.evalAux?_prefixAcceptanceCopiesBuild_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) (x : BitString n) (choices : Fin runs → BitString T) (wires : Array Bool) (hsize : wires.size = primaryAvailable) (hdata : ∀ (j : Fin n), wires[↑(layout.data j)]? = some (x j)) (hchoices : ∀ (j : Fin runs) (t : Fin T), wires[↑(layout.choice j t)]? = some (choices j t)) (i : ℕ) (hi : i ≤ runs) : ∃ (result : Array Bool), (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).circuit.evalAux? wires = some result ∧ result.size = (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).available primaryAvailable ∧ (∀ j < wires.size, result[j]? = wires[j]?) ∧ ∀ (j : Fin runs), ↑j < i → result[(prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).verdictWires j]? = some (parallelAcceptanceBits tm T x choices j)

Evaluating the first i acceptance copies succeeds, preserves every primary input, and records the exact bounded acceptance bit for each completed run.

theorem Complexity.CircuitUnrolling.evalAux?_acceptanceCopiesFragment_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) (x : BitString n) (choices : Fin runs → BitString T) (wires : Array Bool) (hsize : wires.size = primaryAvailable) (hdata : ∀ (j : Fin n), wires[↑(layout.data j)]? = some (x j)) (hchoices : ∀ (j : Fin runs) (t : Fin T), wires[↑(layout.choice j t)]? = some (choices j t)) : ∃ (result : Array Bool), (acceptanceCopiesFragment tm runs T n primaryAvailable layout).evalAux? wires = some result ∧ result.size = wires.size + acceptanceCopiesSize tm runs T n primaryAvailable layout ∧ (∀ j < wires.size, result[j]? = wires[j]?) ∧ ∀ (j : Fin runs), result[acceptanceCopiesVerdictWires tm runs T n primaryAvailable layout j]? = some (parallelAcceptanceBits tm T x choices j)

Evaluating all independent acceptance copies appends their exact gate count and populates every recorded verdict wire.

theorem Complexity.CircuitUnrolling.evalAux?_amplifiedAcceptanceRawCircuit_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) (x : BitString n) (choices : Fin runs → BitString T) (wires : Array Bool) (hsize : wires.size = primaryAvailable) (hdata : ∀ (j : Fin n), wires[↑(layout.data j)]? = some (x j)) (hchoices : ∀ (j : Fin runs) (t : Fin T), wires[↑(layout.choice j t)]? = some (choices j t)) : ∃ (result : Array Bool), (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout).evalAux? wires = some result ∧ result.size = wires.size + List.length (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout) ∧ (∀ j < wires.size, result[j]? = wires[j]?) ∧ result[amplifiedAcceptanceOutputWire tm runs T n primaryAvailable layout]? = some (decide (strictMajorityThreshold runs ≤ Fin.countP (parallelAcceptanceBits tm T x choices)))

Evaluating the complete amplified circuit feeds the independent bounded acceptance bits to the strict-majority threshold fragment.

theorem Complexity.CircuitUnrolling.eval?_amplifiedAcceptanceRawCircuit_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) (x : BitString n) (choices : Fin runs → BitString T) (input : BitString primaryAvailable) (hdata : ∀ (j : Fin n), input (layout.data j) = x j) (hchoices : ∀ (j : Fin runs) (t : Fin T), input (layout.choice j t) = choices j t) : (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout).eval? input.toList = some (decide (strictMajorityThreshold runs ≤ Fin.countP (parallelAcceptanceBits tm T x choices)))

Raw single-output evaluation returns the threshold predicate over all independent bounded acceptance bits.

theorem Complexity.CircuitUnrolling.eval?_canonicalAmplifiedAcceptanceRawCircuit_internal {k : ℕ} (tm : NTM k) (runs T n : ℕ) [NeZero (runs * T + n)] (seed : BitString (runs * T)) (x : BitString n) : (canonicalAmplifiedAcceptanceRawCircuit tm runs T n).eval? (BitString.toList (Fin.append seed x)) = some (decide (strictMajorityThreshold runs ≤ Fin.countP (canonicalAcceptanceBits tm runs T x seed)))

Under the canonical flattened-seed layout, raw evaluation returns the threshold predicate over the named canonical acceptance-bit vector.