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
• mem_FP_of_bounded_key, FPPred.of_bounded_key — any value or test of a polynomial-time key of bounded length is polynomial-time
• CobhamFP_eq_FP — Cobham's machine-independent characterization of FP
• iterate_mem_FP, iterate_mem_FP_of_polyBound, iterate_mem_FP_of_step_le, iterate_mem_FP_along — iterating a polynomial-time step is polynomial-time while the states stay polynomially short
• recFold_mem_FP_of_bound — so is a bitwise fold with polynomially short states
• catRange_mem_FP, flatMap_range_mem_FP — concatenating a polynomial-time rule's outputs over a unary range is polynomial-time, with corollaries for list encodings, counts, bounded search, maxima and bitwise descriptions
• UnaryFn, FPPred — closure rules for polynomial-time functions to ℕ (written in unary) and polynomial-time tests: arithmetic, comparisons, connectives, case distinction, bounded loops, division, capped powers and logarithms
• FPPred.forall_lt, FPPred.exists_lt — quantifying a polynomial-time test over the indices below a polynomial-time number
• getBit_mem_FP, UnaryFn.leadingTrueLength — polynomial-time bit reads and unary-prefix parsing, including missing bits and unterminated prefixes
• toBitsLE_mem_FP, bits_mem_FP, UnaryFn.fromBitsLE_min — writing a polynomial-time number in binary, and reading a binary numeral back below a polynomial-time cap
• encodeList_mem_FP, natEncode_mem_FP — writing the DataEncode encoding of a bit list or of a polynomial-time number

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.