feat(Classes/PP): unbounded-error probabilistic time PPTIME - #1847

Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/

Not declared at the PR head: `PPTIME_mono_of_eventually_le`, `half_lt_eval_runClosed_apply_iff`. Advisory only; see the job summary.

`Turing.MultiTapePTM.DecidesByMajorityInTime` and `Turing.MultiTapePTM.DecidesWithBoundedErrorInTime` (Complexity/Computability/Complexity/Classes/Time.lean:107) share a 435-node subterm, 71% of the smaller body, built from `Turing.MultiTapeMachine.Config`, `Empty`, `Function.Embedding`, `PMF.support`, `Cslib.ProbComp.eval`, `Turing.MultiTapePTM.runClosedConfigFrom`. Advisory only; see the job summary.