Deterministic unrolling families — proof internals

This module proves exact semantics and polynomial size for the family obtained by unrolling a deterministic machine. Public statements are exposed by Complexitylib.Classes.PPoly.Unrolling.

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

Internal exact-horizon correctness of the bounded acceptance predicate for a deterministic decider.

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

Internal semantics of the deterministic unrolling family at every input length, including the explicit length-zero member.

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

Internal fixed-length correctness theorem for a deterministic unrolling family.

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

Internal whole-language correctness theorem for deterministic unrolling.

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

Internal polynomial-size bound for a deterministic unrolling family.

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

Internal packaging theorem: a polynomial-time deterministic decider yields a polynomial-size nonuniform circuit family.

theorem Complexity.P_subset_PPoly_internal : P ⊆ PPoly

Internal direct proof that deterministic polynomial time has nonuniform polynomial-size circuits.