Streamable deterministic unrolling families

This module exposes a deterministic tableau family whose positive members are reconstructed directly from acceptanceRawCircuit. Its circuit code is exactly the encoding of that raw gate list, avoiding the repeated typed hardwiring used by the older nonuniform family. This is the code target for the log-space uniformity emitter.

Main results

• TM.directUnrollingCircuitFamily_function — exact bounded-trace semantics.
• TM.directUnrollingCircuitFamily_encodeAt_zero — explicit empty-input code.
• TM.directUnrollingCircuitFamily_encodeAt_succ — exact raw serialization.
• TM.directUnrollingCircuitFamily_encodeAt — total exact code specification.
• TM.DecidesInTime.directUnrollingCircuitFamily_decides — language correctness.
• TM.directUnrollingCircuitFamily_size_bigO — cubic-in-time size.

@[simp]

theorem Complexity.CircuitUnrolling.deterministicInputWires_choice_val (T n : ℕ) [NeZero n] (i : Fin T) : ↑((deterministicInputWires T n).choice i) = 0

Every deterministic choice position reuses primary input wire zero.

@[simp]

theorem Complexity.CircuitUnrolling.deterministicInputWires_data (T n : ℕ) [NeZero n] (i : Fin n) : (deterministicInputWires T n).data i = i

Deterministic unrolling leaves every data input at its original wire.

theorem Complexity.TM.directUnrollingCircuitFamily_function {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) (x : BitString n) : (tm.directUnrollingCircuitFamily f).function n x = CircuitUnrolling.boundedAcceptanceBit tm.toNTM (f n) x fun (x : Fin (f n)) => false

The direct deterministic family computes the exact bounded acceptance bit.

theorem Complexity.TM.directUnrollingCircuitFamily_encodeAt_zero {k : ℕ} (tm : TM k) (f : ℕ → ℕ) : (tm.directUnrollingCircuitFamily f).encodeAt 0 = [false, CircuitUnrolling.boundedAcceptanceBit tm.toNTM (f 0) (fun (i : Fin 0) => i.elim0) fun (x : Fin (f 0)) => false]

At length zero, the direct family code is the tag followed by the fixed bounded-run answer bit.

theorem Complexity.TM.directUnrollingCircuitFamily_encodeAt_succ {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) : (tm.directUnrollingCircuitFamily f).encodeAt (n + 1) = true :: (tm.directUnrollingRawCircuit f (n + 1)).encode

At every positive length, the family code is literally the tagged encoding of the direct raw tableau circuit.

theorem Complexity.TM.directUnrollingCircuitFamily_encodeAt {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) : (tm.directUnrollingCircuitFamily f).encodeAt n = tm.directUnrollingCode f n

The family codec agrees at every length with the explicit direct code map, including the separate zero-length member.

theorem Complexity.TM.DecidesInTime.directUnrollingCircuitFamily_decides {k : ℕ} {tm : TM k} {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInTime L f) : (tm.directUnrollingCircuitFamily f).Decides L

A deterministic decider's direct tableau family decides the same language.

theorem Complexity.TM.directUnrollingCircuitFamily_size_bigO {k : ℕ} (tm : TM k) {f : ℕ → ℕ} {d : ℕ} (hf : BigO f fun (x : ℕ) => x ^ d) : BigO (tm.directUnrollingCircuitFamily f).size fun (x : ℕ) => x ^ (3 * d)

A horizon in O(n^d) gives the direct family size O(n^(3d)).