Closure of P under FP preimages — proof internals

The preprocessing function and target decider are first normalized to natural-polynomial time bounds. Their executable sequential composition then decides the preimage language within the polynomial obtained by composing those bounds.

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

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