feat: Cobham characterization of FP

Complexitylib/Asymptotics/PolyBound.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+module
+public import Complexitylib.Asymptotics
+
+/-!
+# Polynomial bounds on natural-number functions
+
+`PolyBound f` says `f` is dominated pointwise (at every argument, not merely
+eventually) by the evaluation of a natural polynomial. Resource bookkeeping
+assembles time and space bounds by addition, multiplication, and monotonicity,
+so an everywhere-bound closed under those operations is easier to carry through
+a construction than a big-O statement; `PolyBound.bigO` converts to the big-O
+form the complexity classes are stated in.
+
+## Main results
+
+- `PolyBound` — pointwise domination by a natural polynomial
+- `PolyBound.const`, `.id`, `.add`, `.mul`, `.pow`, `.mono`, `.max`, `.eval` —
+  the closure API
+- `PolyBound.bigO` — a polynomial bound is a big-O power bound
+-/
+
+
+@[expose] public section
+
+namespace Complexity
+
+/-- Pointwise domination by the evaluation of a natural polynomial. -/
+def PolyBound (f : ℕ → ℕ) : Prop :=
+  ∃ p : Polynomial ℕ, ∀ inputLength, f inputLength ≤ p.eval inputLength
+
+namespace PolyBound
+
+theorem const (value : ℕ) : PolyBound (fun _ => value) :=
+  ⟨Polynomial.C value, fun _ => by simp⟩
+
+theorem id : PolyBound (fun inputLength => inputLength) :=
+  ⟨Polynomial.X, fun _ => by simp⟩
+
+theorem add {f g : ℕ → ℕ} (hf : PolyBound f) (hg : PolyBound g) :
+    PolyBound (fun inputLength => f inputLength + g inputLength) := by
+  obtain ⟨p, hp⟩ := hf
+  obtain ⟨q, hq⟩ := hg
+  exact ⟨p + q, fun inputLength => by
+    rw [Polynomial.eval_add]
+    exact Nat.add_le_add (hp inputLength) (hq inputLength)⟩
+
+theorem mul {f g : ℕ → ℕ} (hf : PolyBound f) (hg : PolyBound g) :
+    PolyBound (fun inputLength => f inputLength * g inputLength) := by
+  obtain ⟨p, hp⟩ := hf
+  obtain ⟨q, hq⟩ := hg
+  exact ⟨p * q, fun inputLength => by
+    rw [Polynomial.eval_mul]
+    exact Nat.mul_le_mul (hp inputLength) (hq inputLength)⟩
+
+theorem mono {f g : ℕ → ℕ} (hg : PolyBound g)
+    (hle : ∀ inputLength, f inputLength ≤ g inputLength) : PolyBound f := by
+  obtain ⟨p, hp⟩ := hg
+  exact ⟨p, fun inputLength => le_trans (hle inputLength) (hp inputLength)⟩
+
+theorem max {f g : ℕ → ℕ} (hf : PolyBound f) (hg : PolyBound g) :
+    PolyBound (fun inputLength => max (f inputLength) (g inputLength)) :=
+  (hf.add hg).mono fun _ => Nat.max_le.mpr
+    ⟨Nat.le_add_right _ _, Nat.le_add_left _ _⟩
+
+theorem eval (p : Polynomial ℕ) :
+    PolyBound (fun inputLength => p.eval inputLength) :=
+  ⟨p, fun _ => le_rfl⟩
+
+theorem pow {f : ℕ → ℕ} (hf : PolyBound f) (exponent : ℕ) :
+    PolyBound (fun inputLength => f inputLength ^ exponent) := by
+  induction exponent with
+  | zero => simpa using const 1
+  | succ exponent ih => simpa [pow_succ] using ih.mul hf
+
+/-- A polynomial bound is a big-O bound by the polynomial's degree. -/
+theorem bigO {f : ℕ → ℕ} (hf : PolyBound f) : ∃ d, f =O (· ^ d) := by
+  obtain ⟨p, hp⟩ := hf
+  exact ⟨p.natDegree, BigO.of_polynomial_bound p hp⟩
+
+end PolyBound
+
+end Complexity

Complexitylib/Classes/P.lean

@@ -12,6 +12,7 @@ public import Complexitylib.Classes.P.PairWithInput
 public import Complexitylib.Classes.P.Preimage
 public import Complexitylib.Classes.P.UnaryLength
 public import Complexitylib.Classes.P.FinsetDomain
+public import Complexitylib.Classes.P.Cobham
 public import Complexitylib.Models.TuringMachine.Subroutines.CopyOutput
 
 /-!
@@ -36,6 +37,7 @@ This file aggregates the definitions and theorems for P, FP, and PSPACE.
 - `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`
+- `CobhamFP_eq_FP` — Cobham's machine-independent characterization of `FP`
 -/
 
 

Complexitylib/Classes/P/Cobham.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+module
+public import Complexitylib.Classes.P.Cobham.Defs
+public import Complexitylib.Classes.P.Defs
+import Complexitylib.Classes.P.Cobham.Internal
+
+/-!
+# Cobham's characterization of FP — surface layer
+
+Cobham's theorem (1965): the machine-independent function algebra
+`Complexity.Cobham` of `Complexitylib.Classes.P.Cobham.Defs` carves out exactly
+the polynomial-time computable string functions.
+
+## Main results
+
+- `CobhamFP_subset_FP` — every function of the algebra is polynomial-time
+- `FP_subset_CobhamFP` — every polynomial-time function is in the algebra
+- `CobhamFP_eq_FP` — **Cobham's theorem**, the two directions together
+
+## How the two directions are proved
+
+Both halves live in `Complexitylib.Classes.P.Cobham.Internal`.
+
+*Soundness* is the induction `Cobham f → FPn f` over the six constructors, where
+`Cobham.FPn` lifts `FP` to argument vectors through the tuple encoding
+`Cobham.encodeVec`. Four constructors are bespoke transducers
+(`Cobham.cons_mem_FP`, `fstBlock_mem_FP`, `sndBlock_mem_FP`, `reorder_mem_FP`,
+`mulLenFn_mem_FP`); the fifth, `boundedRec`, is a loop: recursion on notation is
+a fold (`Cobham.recFold_eq_recNotation`), Cobham's side condition makes its width
+clamp vacuous (`Cobham.recFoldClamp_eq_recFold`), and `Cobham.iterate_mem_FP`
+runs the clamped step once per bit under a polynomial ruler.
+
+*Completeness* simulates a polynomial-time machine inside the algebra. A whole
+configuration is one block-aligned bitstring with each tape split at its head, so
+a head move is a two-bit shift (`Cobham.cfgCode`); the transition function is the
+finite table `Cobham.stepFn`; the run is `Cobham.iterFn` under a clock built from
+`smash` (`Cobham.exists_pow_clock`); and the output is read off the output tape
+after a rewind (`Cobham.rewindFn`). The assembly is `Cobham.simFn_eq`.
+-/
+
+
+@[expose] public section
+
+namespace Complexity
+
+/-- Cobham's algebra is sound for polynomial time: every function of the (unary
+fragment of the) algebra is computable by a deterministic TM in polynomial time.
+
+The multi-arity soundness induction `Cobham.cobham_imp_FPn`, specialized to
+arity one. -/
+theorem CobhamFP_subset_FP : CobhamFP ⊆ FP :=
+  Cobham.CobhamFP_subset_FP_of_FPn
+
+/-- Cobham's algebra is complete for polynomial time: every polynomial-time
+computable function belongs to the algebra.
+
+Proved by simulating the machine inside the algebra (`Cobham.simFn_eq`). -/
+theorem FP_subset_CobhamFP : FP ⊆ CobhamFP :=
+  Cobham.FP_subset_CobhamFP_internal
+
+/-- **Cobham's theorem** (1965): the machine-independent function algebra of
+`Complexitylib.Classes.P.Cobham.Defs` characterizes exactly the polynomial-time
+computable string functions. -/
+theorem CobhamFP_eq_FP : CobhamFP = FP :=
+  Set.Subset.antisymm CobhamFP_subset_FP FP_subset_CobhamFP
+
+end Complexity

Complexitylib/Classes/P/Cobham/Defs.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+module
+public import Mathlib.Data.Fin.Tuple.Basic
+public import Mathlib.Data.List.Basic
+
+/-!
+# Cobham's characterization of FP — definitions
+
+This file defines Cobham's machine-independent characterization of the polynomial-time
+computable functions on bitstrings (Cobham, *The intrinsic computational difficulty of
+functions*, 1965): the smallest class of functions `(Fin n → List Bool) → List Bool`
+containing the projections, the empty string, the two bit successors, and the smash
+function, and closed under composition and **limited recursion on notation**.
+
+Bitstrings are LSB-first: in the recursion on notation, the head of the list is the
+least-significant (innermost) bit, so the bit successors *prepend* a bit
+(`x ↦ b :: x`, the string analogue of `n ↦ 2·n + bit`), and recursion on notation
+peels bits off the head.
+
+The functions are multi-arity (indexed by `Fin n` argument vectors) because limited
+recursion on notation inherently produces functions of higher arity; the unary fragment
+is collected in `CobhamFP`, which `Complexitylib.Classes.P.Cobham` proves equal to the
+machine class `FP`.
+
+## Main definitions
+
+- `Complexity.smash` — Cobham's smash function: a string of length `|x| · |y|`
+- `Complexity.recNotation` — the recursion-on-notation combinator
+- `Complexity.Cobham` — the inductive predicate carving out Cobham's function algebra
+- `Complexity.CobhamFP` — the unary fragment, as a set of string functions
+
+## Design notes
+
+The bound in `Cobham.boundedRec` follows Cobham's original formulation: the recursively
+defined function must be *length-bounded by another function of the class* (rather than
+by an external polynomial). Together with `smash` and the successors this realizes
+exactly the polynomial length bounds, which is what makes the class no larger than `FP`;
+dropping the bound would admit iterated doubling and hence exponential growth.
+
+The string toolkit the proof is written in — bit dispatch, flags, fixed-width blocks
+— is not part of this statement and lives in
+`Complexitylib.Classes.P.Cobham.Internal.Blocks`.
+-/
+
+
+@[expose] public section
+
+namespace Complexity
+
+/-- **Cobham's smash function** on bitstrings: a canonical string of length
+`|x| · |y|`. This is the length-arithmetic engine of the class: composing `smash` with
+the bit successors and projections realizes every polynomial length bound, which is
+what lets `Cobham.boundedRec` bound recursions by a function of the class itself.
+
+(Cobham's original smash is `x # y = 2^(|x|·|y|)`; over bitstrings we keep only the
+length, which is all the class ever uses.) -/
+def smash (x y : List Bool) : List Bool :=
+  List.replicate (x.length * y.length) false
+
+@[simp] theorem smash_length (x y : List Bool) :
+    (smash x y).length = x.length * y.length := by
+  simp [smash]
+
+
+/-- **Recursion on notation**: the string analogue of primitive recursion, recursing on
+the bit structure of the first argument.
+
+`recNotation g h₀ h₁ x v` computes `g v` when `x` is empty, and on `b :: x` applies the
+step function selected by the bit `b` to the argument vector consisting of the tail
+`x`, the recursive value on the tail, and the parameters `v`. -/
+def recNotation {n : ℕ} (g : (Fin n → List Bool) → List Bool)
+    (h₀ h₁ : (Fin (n + 2) → List Bool) → List Bool) :
+    List Bool → (Fin n → List Bool) → List Bool
+  | [], v => g v
+  | b :: x, v =>
+      (bif b then h₁ else h₀) (Fin.cons x (Fin.cons (recNotation g h₀ h₁ x v) v))
+
+@[simp] theorem recNotation_nil {n : ℕ} (g : (Fin n → List Bool) → List Bool)
+    (h₀ h₁ : (Fin (n + 2) → List Bool) → List Bool) (v : Fin n → List Bool) :
+    recNotation g h₀ h₁ [] v = g v := rfl
+
+@[simp] theorem recNotation_cons {n : ℕ} (g : (Fin n → List Bool) → List Bool)
+    (h₀ h₁ : (Fin (n + 2) → List Bool) → List Bool) (b : Bool) (x : List Bool)
+    (v : Fin n → List Bool) :
+    recNotation g h₀ h₁ (b :: x) v =
+      (bif b then h₁ else h₀) (Fin.cons x (Fin.cons (recNotation g h₀ h₁ x v) v)) := rfl
+
+/-- **Cobham's function algebra**: the smallest class of bitstring functions containing
+the projections, the empty string, the bit successors `x ↦ b :: x`, and `smash`, and
+closed under composition and limited recursion on notation.
+
+In `boundedRec`, the recursion is *limited*: the result must be length-bounded,
+uniformly in the arguments, by a function `j` already in the class. This is the
+polynomial-growth leash that pins the class to exactly `FP`
+(see `Complexitylib.Classes.P.Cobham`). -/
+inductive Cobham : ∀ {n : ℕ}, ((Fin n → List Bool) → List Bool) → Prop
+  /-- Every projection is in the class. -/
+  | proj {n : ℕ} (i : Fin n) : Cobham fun v => v i
+  /-- The empty-string constant (at every arity) is in the class. -/
+  | empty {n : ℕ} : Cobham fun _ : Fin n → List Bool => []
+  /-- The bit successors `x ↦ b :: x` (the string analogue of `n ↦ 2·n + b`) are in
+  the class. -/
+  | bit (b : Bool) : Cobham fun v : Fin 1 → List Bool => b :: v 0
+  /-- The smash function is in the class. -/
+  | smash : Cobham fun v : Fin 2 → List Bool => smash (v 0) (v 1)
+  /-- The class is closed under composition. -/
+  | comp {m n : ℕ} {f : (Fin m → List Bool) → List Bool}
+      {gs : Fin m → (Fin n → List Bool) → List Bool} :
+      Cobham f → (∀ i, Cobham (gs i)) → Cobham fun v => f fun i => gs i v
+  /-- The class is closed under **limited recursion on notation**: recursion on the bit
+  structure of the first argument, provided the result is length-bounded by a function
+  `j` of the class. -/
+  | boundedRec {n : ℕ} {g : (Fin n → List Bool) → List Bool}
+      {h₀ h₁ : (Fin (n + 2) → List Bool) → List Bool}
+      {j : (Fin (n + 1) → List Bool) → List Bool} :
+      Cobham g → Cobham h₀ → Cobham h₁ → Cobham j →
+      (∀ x v, (recNotation g h₀ h₁ x v).length ≤ (j (Fin.cons x v)).length) →
+      Cobham fun v : Fin (n + 1) → List Bool => recNotation g h₀ h₁ (v 0) (Fin.tail v)
+
+/-- The unary fragment of Cobham's function algebra, as a class of string functions.
+`Complexitylib.Classes.P.Cobham` proves `CobhamFP = FP`: this machine-independent
+algebra carves out exactly the polynomial-time computable functions. -/
+def CobhamFP : Set (List Bool → List Bool) :=
+  {f | Cobham fun v : Fin 1 → List Bool => f (v 0)}
+
+end Complexity