Streamable deterministic unrolling families — proof internals

This module proves that the direct raw family has the same deterministic trace semantics and cubic size bound as the fixed-choice family, while exposing an exact positive-length serialization theorem.

@[simp]

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

@[simp]

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

theorem Complexity.TM.directUnrollingCircuitFamily_function_internal {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

Internal semantics of the direct deterministic unrolling family.

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

Internal exact positive-member serialization through the raw tableau.

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

Internal exact serialization theorem at every input length.

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

Internal whole-language correctness of the direct deterministic family.

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

Internal cubic size estimate for the direct deterministic family.