P — surface layer

This file aggregates the definitions and theorems for P, FP, and PSPACE.

Definitions (from P/Defs.lean)

• P — polynomial time: ⋃ k, DTIME(n^k)
• FP — functions computable in polynomial time
• PSPACE — polynomial space: ⋃ k, DSPACE(n^k)

Theorems

• DTIME_union — DTIME is closed under union (AB Claim 1.5)
• id_mem_FP — the identity function is computable in linear time
• mem_P_iff_decidesInTime_polynomial — polynomial-evaluation normal form for P
• mem_FP_iff_computesInTime_polynomial — polynomial-evaluation normal form
• mem_FP_comp — FP is closed under function composition
• mem_FP_pairWithInput — an FP result can be paired with its original input
• mem_P_preimage — P is closed under preimages of functions in FP
• unaryLength_mem_FP — materializing the unary input length belongs to FP
• ite_mem_finset_mem_FP — functions supported on a finite set belong to FP

theorem Complexity.DTIME_union {T₁ T₂ : ℕ → ℕ} {L₁ L₂ : Language} (h₁ : L₁ ∈ DTIME T₁) (h₂ : L₂ ∈ DTIME T₂) : L₁ ∪ L₂ ∈ DTIME fun (n : ℕ) => T₁ n + T₂ n

DTIME is closed under union (AB Claim 1.5): if L₁ ∈ DTIME(T₁) and L₂ ∈ DTIME(T₂), then L₁ ∪ L₂ ∈ DTIME(T₁ + T₂).

theorem Complexity.id_mem_FP : id ∈ FP

The identity function belongs to FP. The executable copyInputToOutputTM copies the input to the output in n + 2 steps, and this concrete bound is linear.