Eventual growth bounds for circuit resources

Polynomial resource bounds and exponential lower bounds meet repeatedly in circuit complexity. This module records the elementary asymptotic bridge in the generic Circuit.Resource namespace: every fixed natural monomial, including its coefficient, is eventually dominated by 2^n.

theorem Cslib.Circuits.Circuit.Resource.eventually_const_mul_pow_le_two_pow (constant degree : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, constant * n ^ degree ≤ 2 ^ n

Every fixed natural polynomial monomial, including a fixed coefficient, is eventually bounded by the matching binary exponential.