Cobham's characterization of FP — proof internals

The assembly of CobhamFP = FP (Complexitylib.Classes.P.Cobham). Not meant for human review of the mathematics — the surface file carries the auditable statements; the type checker carries this.

The machines are in sibling modules (Internal.BlockScan, Internal.Cat, Internal.ConsBit, Internal.Reorder, Internal.MulLen, Internal.Iterate), the algebra toolkit in Internal.Algebra, and the interpreter of the completeness direction in Internal.Encoding, Internal.StepAlgebra, Internal.Extract and Internal.Simulate. What remains here is the soundness induction and the boundedRec loop.

Contents

• the six constructor cases fpn_empty, fpn_proj, fpn_bit, fpn_smash, fpn_comp, fpn_boundedRec, and the induction cobham_imp_FPn over them;
• the FP closure lemmas they need: pairFn_mem_FP, appendFn_mem_FP, selectHeadFn_mem_FP (branching on a bit, via Complexity.headFlag), takeLenFn_mem_FP, assembleVec_mem_FP;
• the boundedRec loop: recNotation_eq_foldr, recFold_eq_recNotation, recFoldClamp_eq_recFold, loopStep_iterate and recFoldClamp_mem_FP, on top of iterate_mem_FP;
• the rulers exists_ruler and exists_exact_ruler that carry the loop's width clamp as data.

The canonical tuple encoding is in the algebra

theorem Complexity.Cobham.encodeVec_mem_internal {n : ℕ} : Cobham encodeVec

The nested tuple encoding is a Cobham function at every fixed arity.

Soundness: Cobham f → FPn f, constructor by constructor

theorem Complexity.Cobham.fpn_empty {n : ℕ} : FPn fun (x : Fin n → List Bool) => []

empty case: the constant empty function is FPn at every arity, witnessed by const_nil_mem_FP.

theorem Complexity.Cobham.fpn_proj {n : ℕ} (i : Fin n) : FPn fun (v : Fin n → List Bool) => v i

proj case: extracting the i-th component of an encoded vector is FP.

The extraction is sndBlock after i-fold fstBlock: peel i leading blocks to reach the encoding of components i, i+1, …, then read its head with sndBlock. Proved here by induction on the arity; each atomic step is FP (fstBlock_mem_FP, sndBlock_mem_FP) and FP is closed under composition (mem_FP_comp), so only those two machine lemmas remain open.

theorem Complexity.Cobham.fpn_bit (b : Bool) : FPn fun (v : Fin 1 → List Bool) => b :: v 0

bit case: prepending a fixed bit is FPn at arity one. On the arity-one encoding encodeVec ![x] = pair [] x, the head component x is sndBlock, so the witness is (b :: ·) ∘ sndBlock; both factors are FP.

theorem Complexity.Cobham.pairFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => pair (a z) (b z)) ∈ FP

Pairing two FP functions of the same input is FP.

Built without a two-output machine: mem_FP_pairWithInput gives the nested triple z ↦ pair (a z) (pair (b z) z) (pairing each computed value against the raw input, then again), and the self-contained reorder drops the trailing input copy to leave pair (a z) (b z). This is what lets fpn_comp avoid a bespoke tuple-assembly machine.

theorem Complexity.Cobham.appendFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => a z ++ b z) ∈ FP

FP is closed under concatenation.

theorem Complexity.Cobham.mulLenFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => List.replicate ((a z).length * (b z).length) false) ∈ FP

Emitting |a z| · |b z| copies of false is FP when a, b are. This zero-filled ruler is an internal length-arithmetic helper, not Cobham's public all-one smash. It is built as the self-contained mulUnpair (see Complexitylib.Classes.P.Cobham.Internal.MulLen) after pairFn a b.

theorem Complexity.Cobham.takeLenFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => List.take (a z).length (b z)) ∈ FP

Truncating one FP value to another's length.

def Complexity.Cobham.selectHead (s x y : List Bool) : List Bool

Select x or y according to the leading bit of s; nothing when s is empty. This is the only shape of value-dependent branching the algebra's loop needs, and Complexity.headFlag is what makes it expressible.

Equations

• Complexity.Cobham.selectHead s x y = if s.head? = some true then x else if s.head? = some false then y else []

theorem Complexity.Cobham.selectHead_eq (s x y : List Bool) : selectHead s x y = List.take ((headFlag true s).length * x.length) x ++ List.take ((headFlag false s).length * y.length) y

Selection is masking. Exactly one of the two masks is full width, so the concatenation returns exactly one branch.

theorem Complexity.Cobham.selectHeadFn_mem_FP {f a b : List Bool → List Bool} (hf : f ∈ FP) (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => selectHead (f z) (a z) (b z)) ∈ FP

Selecting between two FP values by a bit is FP.

theorem Complexity.Cobham.fpn_smash : FPn fun (v : Fin 2 → List Bool) => Complexity.smash (v 0) (v 1)

smash case: the smash function is FPn. On encodeVec ![x, y] the two components are sndBlock and sndBlock ∘ fstBlock; smash x y is |x| · |y| copies of true, so the witness first computes a zero-filled ruler with mulLenFn_mem_FP and then applies unaryLength_mem_FP.

theorem Complexity.Cobham.assembleVec_mem_FP {m : ℕ} (w : Fin m → List Bool → List Bool) (hw : ∀ (i : Fin m), w i ∈ FP) : (fun (z : List Bool) => encodeVec fun (i : Fin m) => w i z) ∈ FP

Assembling an encoded vector out of FP component functions of a common input is FP. Proved by induction on the arity: the empty vector is the constant [], and the successor step is one pairFn_mem_FP.

theorem Complexity.Cobham.fpn_comp {m n : ℕ} {f : (Fin m → List Bool) → List Bool} {gs : Fin m → (Fin n → List Bool) → List Bool} (ihf : FPn f) (ihgs : ∀ (i : Fin m), FPn (gs i)) : FPn fun (v : Fin n → List Bool) => f fun (i : Fin m) => gs i v

comp case: FPn is closed under Cobham composition. On encodeVec v, each inner gs i is computed by its FP witness G i, the results are assembled into encodeVec (fun i => gs i v) (assembleVec_mem_FP), and the outer f's witness is applied; FP is closed under composition. Rests only on pairFn_mem_FP.

def Complexity.Cobham.recNotationStep {n : ℕ} (h₀ h₁ : (Fin (n + 2) → List Bool) → List Bool) (w : Fin n → List Bool) (b : Bool) (p : List Bool × List Bool) : List Bool × List Bool

One step of recursion on notation viewed as a fold operation: extend the running suffix p.1 by the bit b and update the running recursive value p.2 by the bit-selected step function. Folding this over a string with List.foldr reproduces recNotation (see recNotation_eq_foldr); it is the per-iteration body a loop machine runs.

Equations

• Complexity.Cobham.recNotationStep h₀ h₁ w b p = (b :: p.1, (bif b then h₁ else h₀) (Fin.cons p.1 (Fin.cons p.2 w)))

theorem Complexity.Cobham.recNotationStep_foldr_fst {n : ℕ} (g : (Fin n → List Bool) → List Bool) {h₀ h₁ : (Fin (n + 2) → List Bool) → List Bool} (s : List Bool) (w : Fin n → List Bool) : (List.foldr (recNotationStep h₀ h₁ w) ([], g w) s).1 = s

The first component of the recursion-on-notation fold accumulates exactly the bits processed so far — i.e. it rebuilds the input string.

theorem Complexity.Cobham.recNotation_eq_foldr {n : ℕ} (g : (Fin n → List Bool) → List Bool) (h₀ h₁ : (Fin (n + 2) → List Bool) → List Bool) (s : List Bool) (w : Fin n → List Bool) : recNotation g h₀ h₁ s w = (List.foldr (recNotationStep h₀ h₁ w) ([], g w) s).2

Recursion on notation is a fold. recNotation g h₀ h₁ s w is the second component of folding recNotationStep over s from the empty suffix and base value g w. This reduces the boundedRec case to iterating a single step function over the bits of s — exactly what a loop machine computes — and is the target identity for fpn_boundedRec.

The boundedRec loop

The boundedRec case runs the recursion as a loop on encoded arguments: recFold A B e W s threads a running suffix t of s and the running accumulator a through the argument encoding pair (pair W a) t, which is exactly encodeVec (Fin.cons t (Fin.cons a w)) when W = encodeVec w.

A machine cannot run recFold as written: nothing stops the accumulator from doubling in length at every iteration, so intermediate values would need exponential space. recFoldClamp truncates every intermediate value to a prescribed width, which makes the loop unconditionally polynomial-time (recFoldClamp_mem_FP); Cobham's limited-recursion side condition is then exactly what shows the truncation never fires (recFoldClamp_eq_recFold).

def Complexity.Cobham.recFold (A B : List Bool → List Bool) (e W : List Bool) : List Bool → List Bool

The recursion-on-notation loop on encoded arguments: fold the bit-selected step functions A (bit false) and B (bit true) over s, threading the running suffix and accumulator through the argument encoding.

Equations

• Complexity.Cobham.recFold A B e W [] = e
• Complexity.Cobham.recFold A B e W (b :: t) = (bif b then B else A) (Complexity.pair (Complexity.pair W (Complexity.Cobham.recFold A B e W t)) t)

def Complexity.Cobham.recFoldClamp (A B : List Bool → List Bool) (bound : ℕ) (e W : List Bool) : List Bool → List Bool

recFold with every intermediate value truncated to bound bits. This is the loop a machine can actually run: each iteration's state is length-bounded, so the whole loop takes polynomial time.

Equations

• Complexity.Cobham.recFoldClamp A B bound e W [] = List.take bound e
• Complexity.Cobham.recFoldClamp A B bound e W (b :: t) = List.take bound ((bif b then B else A) (Complexity.pair (Complexity.pair W (Complexity.Cobham.recFoldClamp A B bound e W t)) t))

theorem Complexity.Cobham.exists_const_ruler (c : ℕ) : ∃ K ∈ FP, ∀ (z : List Bool), c ≤ (K z).length

An FP function whose output is at least c bits long, for any constant c. Built by iterating pair · [], which doubles the length and adds two.

theorem Complexity.Cobham.exists_pow_ruler (c d : ℕ) : ∃ R ∈ FP, ∀ (z : List Bool), c * (z.length + 1) ^ d ≤ (R z).length

Rulers. For every constant c and exponent d there is an FP function whose output is at least c · (|z| + 1) ^ d bits long. Rulers let the loop of the boundedRec case carry its width clamp as data — truncating to a string costs linear time, whereas truncating to a computed number would not.

theorem Complexity.Cobham.exists_ruler (p : Polynomial ℕ) : ∃ R ∈ FP, ∀ (z : List Bool), Polynomial.eval z.length p ≤ (R z).length

Every polynomial bound has an FP ruler.

Exact rulers

exists_ruler builds an FP string at least p.eval |z| bits long, which is all a clamp needs. The loop needs an exact one: the width it truncates to is the ruler's length, and that has to be the bound the statement names. Exactness comes from Complexity.unaryLength_mem_FP together with the two exact length arithmetic operations now available — mulLenFn_mem_FP multiplies lengths and appendFn_mem_FP adds them.

theorem Complexity.Cobham.const_replicate_mem_FP (c : ℕ) : (fun (x : List Bool) => List.replicate c false) ∈ FP

Constants of any width are FP.

theorem Complexity.Cobham.exists_exact_ruler (p : Polynomial ℕ) : ∃ R ∈ FP, ∀ (z : List Bool), (R z).length = Polynomial.eval z.length p

A ruler of length exactly p.eval |z|.

The loop as an iteration

recFoldClamp is an iteration of a single FP step function on a packed state. Writing s for sndBlock z, the state after m iterations is

pair (pair R (pair W s)) (pair (s.drop (|s| - m)) (recFoldClamp … (s.drop (|s| - m))))

so the answer is the accumulator after |s| iterations. Every ingredient of the step is now FP: the suffix grows by Complexity.takeLen against a ruler one longer, read off s.reverse; the branch on the new leading bit is selectHead; and the clamp is takeLen against R.

def Complexity.Cobham.loopStepOn (A B : List Bool → List Bool) (R W s t a : List Bool) : List Bool

One iteration of the clamped loop, on the loop's components.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.Cobham.loopStep (A B : List Bool → List Bool) (v : List Bool) : List Bool

One iteration of the clamped loop, on the packed state.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.Cobham.loopStep_pair (A B : List Bool → List Bool) (R W s t a : List Bool) : loopStep A B (pair (pair R (pair W s)) (pair t a)) = loopStepOn A B R W s t a

theorem Complexity.Cobham.loopStep_mem_FP {A B : List Bool → List Bool} (hA : A ∈ FP) (hB : B ∈ FP) : loopStep A B ∈ FP

The step is FP.

theorem Complexity.Cobham.loopStep_iterate {A B : List Bool → List Bool} (R W s e : List Bool) (m : ℕ) : m ≤ s.length → (loopStep A B)^[m] (pair (pair R (pair W s)) (pair [] (List.take R.length e))) = pair (pair R (pair W s)) (pair (List.drop (s.length - m) s) (recFoldClamp A B R.length e W (List.drop (s.length - m) s)))

The loop's invariant. After m iterations the state holds the suffix s.drop (|s| - m) and the clamped fold over it.

theorem Complexity.Cobham.recFoldClamp_length_le (A B : List Bool → List Bool) (bound : ℕ) (e W s : List Bool) : (recFoldClamp A B bound e W s).length ≤ bound

The clamp really clamps.

The loop's step function

Complexity.iterate_input_mem_FP supplies a machine that applies an FP function once per bit of its own input, starting from pair [] x. The state below is pair (pair C v) x: a counter C, the running value v, and the machine's input x kept verbatim. Keeping x is what makes the whole construction work: the ruler and the width stay readable at every step, and truncating the new state to |x| bounds the state length globally — the machine's contract needs a bound that holds for every input, not just for the well-formed ones.

def Complexity.Cobham.emptyFlag (s : List Bool) : List Bool

A flag whose leading bit is true exactly when s is empty — the one test Complexity.selectHead cannot make directly.

Equations

• Complexity.Cobham.emptyFlag s = Complexity.headFlag true s ++ Complexity.headFlag false s ++ [true]

@[simp]

theorem Complexity.Cobham.emptyFlag_nil : emptyFlag [] = [true]

theorem Complexity.Cobham.emptyFlag_head_cons (b : Bool) (t : List Bool) : (emptyFlag (b :: t)).head? = some false

theorem Complexity.Cobham.selectHead_emptyFlag_nil (x y : List Bool) : selectHead (emptyFlag []) x y = x

theorem Complexity.Cobham.length_take_le_arg (n : ℕ) (l : List Bool) : (List.take n l).length ≤ n

theorem Complexity.Cobham.selectHead_emptyFlag_cons (b : Bool) (t x y : List Bool) : selectHead (emptyFlag (b :: t)) x y = y

theorem Complexity.Cobham.selectHead_length_le (s x y : List Bool) : (selectHead s x y).length ≤ max x.length y.length

def Complexity.Cobham.nextCounter (w : List Bool) : List Bool

The counter of the next iteration: one more mark of the reversed ruler.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.Cobham.nextValue (F : List Bool → List Bool) (w : List Bool) : List Bool

The value of the next iteration: the initial value on the first step, then F of the current value until the counter saturates.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.Cobham.iterStep (F : List Bool → List Bool) (w : List Bool) : List Bool

One iteration of the loop, truncated to the machine's own input length.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Cobham.sndBlock_iterStep (F : List Bool → List Bool) (w : List Bool) : sndBlock (iterStep F w) = sndBlock w

theorem Complexity.Cobham.iterStep_length_le (F : List Bool → List Bool) (w : List Bool) : (iterStep F w).length ≤ 3 * (sndBlock w).length + 2

theorem Complexity.Cobham.iterStep_iterate_length_le (F : List Bool → List Bool) (x : List Bool) (i : ℕ) : ((iterStep F)^[i] (pair [] x)).length ≤ 3 * x.length + 2

The state length is globally bounded: whatever the input, the state after one or more iterations fits in 3|x| + 2.

theorem Complexity.Cobham.emptyFlag_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (z : List Bool) => emptyFlag (f z)) ∈ FP

theorem Complexity.Cobham.nextCounter_mem_FP : nextCounter ∈ FP

theorem Complexity.Cobham.nextValue_mem_FP {F : List Bool → List Bool} (hF : F ∈ FP) : nextValue F ∈ FP

theorem Complexity.Cobham.iterStep_mem_FP {F : List Bool → List Bool} (hF : F ∈ FP) : iterStep F ∈ FP

def Complexity.Cobham.iterVal (F : List Bool → List Bool) (Krev W v₀ : List Bool) : ℕ → List Bool

The value the loop carries after i iterations, from the second on.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.Cobham.iterVal F Krev W v₀ 0 = v₀

theorem Complexity.Cobham.iterVal_length_le (F : List Bool → List Bool) (Krev W v₀ : List Bool) (i : ℕ) : (iterVal F Krev W v₀ i).length ≤ max v₀.length W.length

theorem Complexity.Cobham.take_succ_min (l : List Bool) (i : ℕ) : List.take (min i l.length + 1) l = List.take (i + 1) l

theorem Complexity.Cobham.iterStep_iterate (F : List Bool → List Bool) (Krev W v₀ : List Bool) (hK : Krev ≠ []) (hfit : ∀ (i : ℕ), (pair (List.take (i + 1) Krev).reverse (iterVal F Krev W v₀ i)).length ≤ (pair (pair Krev W) v₀).length) (i : ℕ) : (iterStep F)^[i + 1] (pair [] (pair (pair Krev W) v₀)) = pair (pair (List.take (i + 1) Krev).reverse (iterVal F Krev W v₀ i)) (pair (pair Krev W) v₀)

The loop's trajectory. With the counter growing one mark per iteration and the state always fitting in the input, the i+1-st state is exactly the counter (Krev.take (i+1)).reverse beside the value iterVal … i.

theorem Complexity.Cobham.counter_take_le (a j : ℕ) (h : j ≤ a) : List.take j (List.replicate a false ++ [true]) = List.replicate j false

theorem Complexity.Cobham.counter_head_false (a j : ℕ) (h1 : 1 ≤ j) (h2 : j ≤ a) : (List.take j (List.replicate a false ++ [true])).reverse.head? = some false

theorem Complexity.Cobham.counter_head_true (a j : ℕ) (h : a + 1 ≤ j) : (List.take j (List.replicate a false ++ [true])).reverse.head? = some true

theorem Complexity.Cobham.iterVal_eq_iterate (F : List Bool → List Bool) (W v₀ : List Bool) (M : ℕ) (hclamp : ∀ j ≤ M, (F^[j] v₀).length ≤ W.length) (i : ℕ) : iterVal F (List.replicate (M + 1) false ++ [true]) W v₀ i = F^[min i M] v₀

The value sequence is the iterate. While the counter has marks left the step applies F; once it saturates the value stops changing. The clamp is a no-op because every intermediate value fits in W.

theorem Complexity.Cobham.iterate_mem_FP {F init ruler width : List Bool → List Bool} (hF : F ∈ FP) (hinit : init ∈ FP) (hruler : ruler ∈ FP) (hwidth : width ∈ FP) (hbound : ∀ (z : List Bool), ∀ n ≤ (ruler z).length, (F^[n] (init z)).length ≤ (width z).length) : (fun (z : List Bool) => F^[(ruler z).length] (init z)) ∈ FP

FP is closed under bounded iteration — the one machine-level fact the soundness direction needs.

Construction. The machine is assembled in Complexitylib.Classes.P.Cobham.Internal.Iterate out of the phase contracts of Complexitylib.Classes.P.Cobham.Internal.IterateLayout; iterate_input_mem_FP is its interface. Three details are worth recording, because three earlier plans died on them.

Why resetting scratch is the crux. F's machine M comes from an existential (F ∈ FP), so nothing is known about the shape it leaves its scratch tapes in. Re-running it needs those tapes genuinely blank, but a content-driven eraser (TM.blankWorkTM scans right to the first blank) under-wipes whenever M left a gap — an isolated blank cell with more content beyond it. TM.wipeStepTM therefore writes blank unconditionally, and Complexity.resetTapesTM drives it a fixed number of times off a fuel register that is unrelated to the wiped tapes' content. TM.reachesIn_work_cells_far supplies the bound that makes the fixed count sufficient: a t-step run cannot have touched anything past head + t. Complexity.iterTail is the resulting five-phase cleanup, shared by the loop body and the setup; its first two phases are not bookkeeping either, since δ_right_of_start only forces a head reading ▷ to move right, so an arbitrary witness machine may legitimately halt with a head at cell 0.

Why the state carries the machine's own input. TM.ComputesInTime quantifies over all inputs, so the loop's contract has to survive malformed ones: the state is pair (pair C v) x with the machine's input x kept verbatim, and every new state is truncated to |x| (iterStep). That makes iterStep_iterate_length_le — a state-length bound holding for every input, not just the well-formed ones — available for free, and keeps the ruler and the width readable at every step. On the intended trajectory the truncation is a no-op (iterStep_iterate).

How the counter avoids a second fuel value. The loop runs |x| + 1 times, one per bit of the machine's own input (TM.inputLenRegTM), which is more iterations than needed; the surplus is absorbed by a counter that grows one mark of Krev = 0^(m+1) 1 per step, whose leading bit turns true exactly when the m real applications are done (counter_head_false, counter_head_true). So iterVal is F iterated min i m times, and over-iteration is harmless (iterVal_eq_iterate). The wipe width is a different register, p.eval |x|, computed by TM.polyEvalTM — the state is longer than the input, so |x| alone cannot pay for the reset.

Time. Each iteration costs iterStep's own polynomial bound at width (width z).length — which is why hbound is a hypothesis — plus the linear copies and the wipe, and there are |x| + 1 of them, so the total is polynomial (polyBnd_iterBound).

theorem Complexity.Cobham.recFoldClamp_mem_FP {A B E : List Bool → List Bool} (hA : A ∈ FP) (hB : B ∈ FP) (hE : E ∈ FP) (p : Polynomial ℕ) : (fun (z : List Bool) => recFoldClamp A B (Polynomial.eval z.length p) (E z) (fstBlock z) (sndBlock z)) ∈ FP

The loop of the boundedRec case. recFoldClamp is loopStep iterated once per bit of sndBlock z (loopStep_iterate), started from the packed state pair (pair R (pair W s)) (pair [] (e.take |R|)) — with R an exact ruler for the clamp (exists_exact_ruler) — and read off with two sndBlocks.

theorem Complexity.Cobham.recFoldClamp_eq_recFold {A B : List Bool → List Bool} {bound : ℕ} {e W : List Bool} (s : List Bool) (hle : ∀ (t : List Bool), t.length ≤ s.length → (recFold A B e W t).length ≤ bound) : recFoldClamp A B bound e W s = recFold A B e W s

Truncation is a no-op as soon as every intermediate value already fits.

theorem Complexity.Cobham.recFold_eq_recNotation {n : ℕ} {g : (Fin n → List Bool) → List Bool} {h₀ h₁ : (Fin (n + 2) → List Bool) → List Bool} {G H₀ H₁ : List Bool → List Bool} (hG : ∀ (u : Fin n → List Bool), G (encodeVec u) = g u) (hH₀ : ∀ (u : Fin (n + 2) → List Bool), H₀ (encodeVec u) = h₀ u) (hH₁ : ∀ (u : Fin (n + 2) → List Bool), H₁ (encodeVec u) = h₁ u) (w : Fin n → List Bool) (s : List Bool) : recFold H₀ H₁ (G (encodeVec w)) (encodeVec w) s = recNotation g h₀ h₁ s w

On encoded arguments the loop computes recursion on notation: recFold over the FP witnesses of g, h₀, h₁ reproduces recNotation.

theorem Complexity.Cobham.output_length_poly_of_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : ∃ (p : Polynomial ℕ), ∀ (x : List Bool), (f x).length ≤ Polynomial.eval x.length p

Every FP function has polynomially bounded output length: a time bound is also an output-length bound (TM.ComputesInTime.output_length_le).

theorem Complexity.Cobham.fpn_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} (ihg : FPn g) (ih0 : FPn h₀) (ih1 : FPn h₁) (ihj : FPn j) (hbound : ∀ (x : List Bool) (v : Fin n → List Bool), (recNotation g h₀ h₁ x v).length ≤ (j (Fin.cons x v)).length) : FPn fun (v : Fin (n + 1) → List Bool) => recNotation g h₀ h₁ (v 0) (Fin.tail v)

boundedRec case: FPn is closed under limited recursion on notation.

By recFold_eq_recNotation the value is the encoded-argument loop recFold run over the bits of v 0. Cobham's limited-recursion side condition hbound caps every intermediate accumulator by |j (…)|, which is polynomial in |encodeVec v| (output_length_poly_of_mem_FP), so the clamped loop recFoldClamp — which a machine can run in polynomial time (recFoldClamp_mem_FP) — never truncates and therefore agrees with recFold.

theorem Complexity.Cobham.cobham_imp_FPn {n : ℕ} {f : (Fin n → List Bool) → List Bool} : Cobham f → FPn f

Soundness induction. Every function of Cobham's algebra is polynomial time on encoded argument vectors.

theorem Complexity.Cobham.CobhamFP_subset_FP_of_FPn : CobhamFP ⊆ FP

Arity-one specialization: from the multi-arity soundness induction, the unary fragment CobhamFP lands in FP.

Completeness: FP ⊆ CobhamFP

theorem Complexity.Cobham.FP_subset_CobhamFP_internal : FP ⊆ CobhamFP

Completeness direction. Every polynomial-time function belongs to Cobham's algebra.

Construction: a polynomial-time Turing machine is simulated inside the algebra.

1. A whole configuration — state, input tape, output tape, work tapes and every head position — is one bitstring of equal-width blocks, each tape split at its head so that a head move is a two-bit shift (Cobham.cfgCode).
2. The one-step transition is a finite case split on (state, symbols read), which is Cobham.tableFn against the finitely many constant key patterns, with each branch built from takeFn/dropFn/appendFn/padFn (Cobham.stepFn). At the halting state the branch is the identity, so the encoding is a fixed point once the machine stops.
3. The step is iterated once per bit of a clock string built from smash (Cobham.exists_pow_clock), long enough by the polynomial normal form mem_FP_iff_computesInTime_polynomial.
4. A second iteration walks the output head back to cell 0 (Cobham.rewindFn), after which that tape's right half-block is the whole tape in order, and the output is read off it by two Complexity.cellBits recursions and one Complexity.runTrue (Cobham.simFn). The length bounds throughout are polynomial, so every boundedRec side condition is met.

theorem Complexity.Cobham.FPn_imp_cobham_internal {n : ℕ} {f : (Fin n → List Bool) → List Bool} (hf : FPn f) : Cobham f

Multi-arity completeness. A unary FP witness on canonical encodings is first translated into the unary Cobham algebra and then composed with encodeVec_mem_internal.