feat: Single Tape Turing Machines (#269)

I have now marked this ready for review but it's quite a large PR,
reviewers please tell me if I should reorganize things or submit in a
different way.

This PR adds a model of Single Tape Turing machines, which inputs and
outputs `List α` for a finite alphabet type `α`, with the following
features:

* In `Cslib/Foundations/Data`
* A file for `StackTape`, a stack-like data structure for optional
alphabet symbols that extends infinitely (in one direction) with blank
(none) symbols. Represented as a finite list that tructates the infinite
stream of none elements
* A file for `BiTape`, a bidirectionally infinite Tape, made from two
`StackTape`
* In `Cslib/Computability/Machines/SingleTapeTuring/Basic.lean`
* `structures` representing computability within a time bound, and
polynomial time computability.
* Machine that computes the identity function, c.f. Mathlib's
[Turing.idComputer](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/TMComputable.html#Turing.idComputer)
* Machine that computes the composition of the function computed by two
individual machines. (Mathlib currently doesn't have this)
	  * Proof this machine preserves polynomial time computation 

This PR was authored with the support of Claude Code and [Project
Numina's Lean MCP fork](https://github.com/project-numina/lean-lsp-mcp)

---

## My Design Notes

While Mathlib has a definition of polynomial time computability based on
a more complicated model of TMs, I think it makes sense to have one
based on a simple single-tape model here.

Longer term, I would like to try to create a unified framework for
talking about TMs with variable amounts of tapes / stacks, so that we
can eventually prove theorems about the time and space overhead incurred
by switching from one model to another (e.g. [2 tape TMs simulate k-tape
TMs with log
overhead](https://www.cs.toronto.edu/tss/files/papers/HennieStearns66.pdf),
1 tape TMs simulate 2-tape TMs with quadratic overhead, 2-stack machines
simulate 1 tape TMs ).

I ultimately did not reuse much if any of the Mathlib infrastructure
around `Tape`s, because of the injectivity issue I described in the
docstring.

---------

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

Author: BoltonBailey

Cslib.lean

@@ -29,6 +29,7 @@ public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Machines.SingleTapeTuring.Basic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs
@@ -39,6 +40,7 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
+public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.FinFun
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.Nat.Segment
@@ -50,6 +52,7 @@ public import Cslib.Foundations.Data.OmegaSequence.Temporal
 public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
+public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS