feat(TimeM): relate timed costs to big-O

[cdbattags]

Mathlib's Asymptotics.IsBigO and IsTheta compare two functions along a filter. TimeM.time is one scalar, so a size-indexed computation does not fit that API by itself.

This adds TimeM.isBigO and TimeM.isTheta in Cslib/Algorithms/Lean/TimeM/Asymptotics.lean. They coerce (cost n).time to ℝ and ask Mathlib whether that function of n is big-O or big-Theta of g at Filter.atTop. The module is separate from TimeM.lean so existing TimeM clients do not import analysis.

lake build Cslib.Algorithms.Lean.TimeM.Asymptotics succeeded, and lake exe mk_all left the new import in Cslib.lean.

Drafted with Grok 4.7, the 500k-context high-effort setting, in Cursor. I used it to read TimeM and Mathlib's Asymptotics.IsBigO / IsTheta and to write these two definitions. This repository has no LLM-generated label; the disclosure above is the step CONTRIBUTING.md asks for, via the Mathlib policy.