Deterministic time has nonuniform circuits

This module specializes bounded NTM acceptance circuits to deterministic machines by fixing the choice prefix of tm.toNTM. It packages the resulting circuits into a family, proves exact language semantics and cubic-in-time size, and concludes P ⊆ P/poly directly from the unrolling construction.

Main results

• TM.unrollingCircuitFamily_function: exact fixed-horizon semantics.
• TM.DecidesInTime.unrollingCircuitFamily_decides: language correctness.
• TM.unrollingCircuitFamily_size_bigO: size O(n^(3d)) for time O(n^d).
• TM.DecidesInTime.mem_PPoly: package one polynomial-time decider.
• P_subset_PPoly: deterministic polynomial time has polynomial-size circuits.

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

The deterministic unrolling family computes the exact bounded acceptance predicate at every input length.

theorem Complexity.TM.DecidesInTime.boundedAcceptanceBit_iff {k : ℕ} {tm : TM k} {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInTime L f) (n : ℕ) (x : BitString n) (choices : BitString (f n)) : CircuitUnrolling.boundedAcceptanceBit tm.toNTM (f n) x choices = true ↔ x.toList ∈ L

A deterministic decider's exact-horizon bounded acceptance bit agrees with language membership, for every choice string of its deterministic embedding.

theorem Complexity.TM.DecidesInTime.unrollingCircuitFamily_function_iff {k : ℕ} {tm : TM k} {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInTime L f) (n : ℕ) (x : BitString n) : (tm.unrollingCircuitFamily f).function n x = true ↔ x.toList ∈ L

A deterministic decider's unrolling family agrees with its language on every fixed-length input.

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

The unrolling family of a deterministic decider decides the same language.

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

If the deterministic horizon is O(n^d), its unrolling family has size O(n^(3d)).

theorem Complexity.TM.DecidesInTime.mem_PPoly {k : ℕ} {tm : TM k} {L : Language} {f : ℕ → ℕ} {d : ℕ} (hdec : tm.DecidesInTime L f) (hf : BigO f fun (x : ℕ) => x ^ d) : L ∈ PPoly

A deterministic decider with a polynomial time horizon decides a language in P/poly through its explicit unrolling family.

theorem Complexity.P_subset_PPoly : P ⊆ PPoly

P ⊆ P/poly, directly by bounded deterministic unrolling.