feat(Classes): prove finitely-supported functions belong to FP

Complexitylib/Classes/P.lean

@@ -10,6 +10,7 @@ import Complexitylib.Classes.P.Composition
 import Complexitylib.Classes.P.PairWithInput
 import Complexitylib.Classes.P.Preimage
 import Complexitylib.Classes.P.UnaryLength
+import Complexitylib.Classes.P.FinsetDomain
 import Complexitylib.Models.TuringMachine.Subroutines.CopyOutput
 
 /-!
@@ -33,6 +34,7 @@ This file aggregates the definitions and theorems for P, FP, and PSPACE.
 - `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`
 -/
 
 namespace Complexity

Complexitylib/Classes/P/FinsetDomain.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Complexitylib.Classes.P.FinsetDomain.Internal
+
+/-!
+# Finite-deviation functions are polynomial-time
+
+A function that agrees with the constant empty-output function on all but
+finitely many inputs is polynomial-time computable. Concretely, for any target
+function `g` and finite set `S`, the function `fun s => if s ∈ S then g s else []`
+belongs to `FP`: the finite lookup table can be hard-wired into the states of a
+Turing machine that decides membership in `S` while scanning the input and then
+emits the corresponding fixed output, all in linear time.
+
+This is the base case for building up polynomial-time functions — every function
+with finite support (relative to the empty output) is trivially in `FP`,
+regardless of how the values `g s` are chosen.
+
+## Main result
+
+- `ite_mem_finset_mem_FP` — `fun s => if s ∈ S then g s else []` belongs to `FP`
+-/
+
+namespace Complexity
+
+/-- A function that agrees with the constant empty-output function except on a
+finite set `S` — that is, `fun s => if s ∈ S then g s else []` — is computable in
+polynomial (indeed linear) time. The finite table of exceptional values is
+hard-wired into the lookup machine's states. -/
+theorem ite_mem_finset_mem_FP (g : List Bool → List Bool) (S : Finset (List Bool)) :
+    (fun s => if s ∈ S then g s else []) ∈ FP :=
+  ite_mem_finset_mem_FP_internal g S
+
+end Complexity