refactor: remove h_mono from PolyTimeComputable.comp

[JohnEdwardJennings]

This PR adds proofs autoformalised by @Aristotle-Harmonic.
Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

Fixes #378

Summary of changes:
Resolved the TODO on lines 487-488 of Cslib/Computability/Machines/SingleTapeTuring/Basic.lean which asked to remove the h_mono : Monotone hg.time_bound assumption from PolyTimeComputable.comp by developing a function to convert a PolyTimeComputable into one with a monotone time bound.

Changes made:

1. Added monotonizeBound — a function that monotonizes f : ℕ → ℕ by taking (Finset.range (n+1)).sup' ... f, i.e. the maximum of f over {0, ..., n}.

2. Added supporting lemmas:

   • monotonizeBound_mono: the monotonized bound is monotone
   • le_monotonizeBound: the original function is bounded by the monotonized version
   • monotonizeBound_le_of_le: if f is bounded by a monotone g, the monotonized f is also bounded by g

3. Added TimeComputable.withMonotoneBound — converts a TimeComputable to one with a monotone time bound using monotonizeBound.

4. Added PolyTimeComputable.withMonotoneBound — converts a PolyTimeComputable to one with a monotone time bound, preserving the polynomial bound (using the fact that Polynomial.eval_mono gives monotonicity of polynomial evaluation over ℕ).

5. Removed h_mono from PolyTimeComputable.comp — the composition now internally monotonizes hg's time bound before passing it to TimeComputable.comp, eliminating the need for the caller to supply a monotonicity proof.

[chenson2018]

@BoltonBailey Could you have a first look at this since it was your TODO comment?