feat(Foundations): define polynomial growth and relate it to big-O

[SamuelSchlesinger]

Following @thomaskwaring's suggestion, defines PolynomiallyBounded f for natural-valued functions by eventual domination by a fixed power n ^ d. Proves equivalence with Mathlib's Asymptotics.IsBigO after casting to the reals, and with a bound c * (n + 1) ^ d valid at every input.

This supplies the growth condition used for polynomial losses and hybrid lengths in the crypto stack. It makes no computability claim.

Originally composed with Claude Code; reworked with Codex to use eventual bounds and Mathlib's asymptotics API.

[thomaskwaring]

There's clearly other review work that needs to be done, but as a first thought is there a reason you didn't use Asymptotics.IsBigO? There's no Norm instance on Nat so you'd need some plumbing, but it's equivalent and you might be able to use the existing lemmas.

[SamuelSchlesinger]

is there a reason you didn't use Asymptotics.IsBigO?

No, I can change it to that and see if that is an improvement.

[thomaskwaring]

actually ∃ d, f ≤[atTop] n ^ d would probably be simpler (i think we should at least have lemmas connecting each version)

[thomaskwaring]

this all looks good to me — i've suggested a few places where i think proofs can be simplified, particularly using grw and looser bounds (since the statement is existential it makes no difference)

also, i don't have a strong opinion either way, but perhaps you could define a trivial norm on Nat which might be fractionally easier than working with the casts

[thomaskwaring]

i think the idiomatic spelling is

Suggested change

	∃ d : ℕ, ∀ᶠ n in atTop, f n ≤ n ^ d
	∃ d : ℕ, f ≤ᶠ[atTop] (· ^ d)

which is defeq

[SamuelSchlesinger]

Yuck :)

[SamuelSchlesinger]

Applied your changes.