feat: Cobham characterization of FP

[BoltonBailey]

This PR defines the Cobham class of efficiently computable functions (consisting of the closure of a certain collection under composition and bounded recursion) and proves this equivalent to FP.

theorem CobhamFP_eq_FP : CobhamFP = FP :=
  Set.Subset.antisymm CobhamFP_subset_FP FP_subset_CobhamFP

People often say they want to do complexity theory or use the class of polynomial time functions, but want to avoid working with Turing machines. The point of this equivalence is to give users an interface where, even though FP is still defined in terms of Turing Machines, proofs about polynomial time computability can avoid Turing machines entirely. Cobham's class is just the set of functions from tuples of bitstrings to bitstrings which include:

• projection functions
• trivial constant and bit concatenation functions
• the "smash" function which is effectively just multiplication in unary.

and which is closed under

• composition
• "bounded recursion" operation of repeating iterating a function over a list, as long as the function does not grow the size of its input too large.

In principle, we should now be able to prove polynomial time computability not by writing a TM, but by proving our function equivalent to a big composition / recursions of functions we already know are polytime.