Closure of NP under polynomial-time preimages — proof internals

The preprocessing function is normalized to a natural-polynomial time bound and composed with a polynomial-time nondeterministic decider through NTM.compositionNTM. The degenerate decider that starts halted accepts nothing, so its language is empty and the preimage is decided without running the composite.

theorem Complexity.mem_NP_iff_decidesInTime_polynomial_internal {L : Language} : L ∈ NP ↔ ∃ (k : ℕ) (N : NTM k) (p : Polynomial ℕ), N.DecidesInTime L fun (x : ℕ) => Polynomial.eval x p

Internal proof that NP membership is equivalent to nondeterministic decision within the evaluation of a natural-coefficient polynomial.

theorem Complexity.language_eq_empty_of_decider_start_halted {k : ℕ} {N : NTM k} {L : Language} {T : ℕ → ℕ} (hN : N.DecidesInTime L T) (hstart : N.qstart = N.qhalt) : L = ∅

A nondeterministic decider that starts halted decides only the empty language: its frozen trace leaves the output tape blank.

theorem Complexity.mem_NP_preimage_internal {f : List Bool → List Bool} {L : Language} (hf : f ∈ FP) (hL : L ∈ NP) : f ⁻¹' L ∈ NP

Internal proof that polynomial-time nondeterministic languages are closed under preimages of polynomial-time string functions.