# Asymptotic resource bounds: proving 3n²+5n+2∈Θ(n²) and ruling out Θ(n) [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-asymptotic-resource-bound/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-asymptotic-resource-bound-01 · production-20261019-adopted-96 ## Goal and scope Let the cost function be f(n)=3n²+5n+2 (n starting at 0), with comparison functions g(n)=n² and h(n)=n. With explicit full-tail witnesses prove f∈O(g) (c=10, N=1) and f∈Ω(g) (c=3, N=0), hence f∈Θ(g); show that N=0 cannot work for O, that c=3 cannot work for O, and that another witness c=4, N=6 also works; then prove f∉O(h), so f∈Ω(h) but f∉Θ(h). Works inside the MKO's scope: n ranges over the natural numbers starting at 0, and the function family and nonnegative coefficients are stated by the exercise (assumption a1); every asymptotic conclusion comes with a full-tail witness and a proof, and finite numeric checks are observations only (assumption a2). Input size and cost model are taken as part of the declaration of f; how a particular algorithm yields f is not discussed, no general polynomial theorem is used, and the canonical MKO and its English edition are not changed. ## Givens and symbols - order_basics - distributive - numeric_evaluation - archimedean - square_nonneg - G1 — The input size n ranges over the natural numbers starting at 0 (MKO assumption a1). - G2 — The cost function f(n)=3n²+5n+2 is declared by the exercise: it is the number of basic operations counted under a fixed cost model and input size; the coefficients 3, 5, 2 are nonnegative. - G3 — Comparison functions g(n)=n² and h(n)=n. - f(n)=3n^2+5n+2 — the declared cost function - g(n)=n^2,\ h(n)=n — the comparison functions - O(g),\ \Omega(g),\ \Theta(g) — the function classes for asymptotic upper bounds, lower bounds and tight bounds - (c,N) — a witness: a constant c>0 and a threshold N - n\ge N — the full tail: every n at least N ## Rules and sources - order_basics · prerequisite — Order of the reals: exactly one of uv holds; u0 give uwvw. - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - archimedean · prerequisite — Archimedean property: for every real x there is a natural number n>x; hence for every ε>0 there is n with 1/n<ε. - square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0. - def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable. - def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true. - add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v). - add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w). - exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x). - forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain. - mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds. - mko_asymptotic_def · cited — For nonnegative functions f,g:N→R, f∈O(g) means that some c>0 and threshold N satisfy f(n)≤c·g(n) for every n≥N; f∈Ω(g) means that some c>0 and N satisfy f(n)≥c·g(n) for every n≥N; f∈Θ(g) requires both. Input size and cost model are part of the claim. · mko-asymptotic-resource-bound - L_n_le_nsq · lemma — For every natural number n≥1: 1≤n≤n². ## Main derivation S01 · definitionBefore f(n)=3n^2+5n+2,\ g(n)=n^2,\ h(n)=n After f(n)>0,\ g(n)\ge 0,\ h(n)\ge 0\ \text{for all}\ n\ge 0 Conditions: n\in\mathbb{N} Rule: def_intro · Uses: G1, G2, G3 Leaf basis: def_intro + square_nonneg + order_basics Name the three functions and confirm the nonnegativity the MKO requires: for n≥0, n²≥0, so 3n²≥0 and 5n≥0, and adding 2>0 gives f(n)>0; g(n)=n²≥0; h(n)=n≥0. The cost model and input size were declared with f (G2), and only functions under this declaration are compared. S02 · equivalentBefore f\in O(g) After \exists c>0\ \exists N\in\mathbb{N}\ \forall n\ge N,\ f(n)\le c\,g(n) Conditions: none Rule: def_unfold · Uses: S01, mko_asymptotic_def Leaf basis: def_unfold + mko_asymptotic_def Unfold the definition of big O: find a witness pair (c,N) such that the whole tail from N on satisfies f(n)≤c·g(n). The quantifier order is 'there exist c and N such that for all n': c and N may not depend on n. The definition of Ω replaces ≤ by ≥, and Θ requires both. S03 · theorem_applicationBefore n\in\mathbb{N},\ n\ge 1 After 1\le n\le n^2 Conditions: n\ge 1 Rule: L_n_le_nsq · Uses: G1 Leaf basis: order_basics + distributive Apply Lemma L_n_le_nsq (proved in S03.1 and S03.2): for n≥1, 1≤n≤n². This lets the lower-order term 5n and the constant 2 be controlled by n². S04 · impliesBefore n\le n^2,\ 1\le n^2\ (n\ge 1) After 5n\le 5n^2,\ 2\le 2n^2\ (n\ge 1) Conditions: n\ge 1; 5>0,\ 2>0 Rule: order_basics · Uses: S03 Leaf basis: order_basics Multiply both sides of n≤n² by the positive number 5, and both sides of 1≤n² by the positive number 2; multiplying by a positive number preserves the direction of an inequality. S05 · impliesBefore f(n)=3n^2+5n+2 After f(n)\le 3n^2+5n^2+2n^2=10n^2\quad(n\ge 1) Conditions: n\ge 1 Rule: order_basics · Uses: S04 Leaf basis: order_basics + distributive + add_assoc Add the two inequalities of S04 to 3n²=3n² (inequalities in the same direction add), giving f(n)≤10n² for every n≥1. Equivalently, 10n²−f(n)=5n(n−1)+2(n²−1), and both terms are nonnegative for n≥1 (N1 checks this as a polynomial identity). S06 · impliesBefore \forall n\ge 1,\ f(n)\le 10\,g(n) After f\in O(g)\ \text{with witness}\ (c,N)=(10,1) Conditions: 10>0 Rule: exists_intro · Uses: S05, S02 Leaf basis: exists_intro + forall_intro S05 was proved for an arbitrary n≥1 with no extra assumption, so by generalization it holds on the whole tail n≥1. Take c=10>0 and N=1; by ∃-introduction and the equivalence of S02, f∈O(g). S07 · impliesBefore n=0 After f(0)=2>0=c\cdot g(0)\ \text{for every}\ c>0 Conditions: none Rule: numeric_evaluation · Uses: G2, G3 Leaf basis: numeric_evaluation + mul_zero The role of the threshold: f(0)=2 while g(0)=0, so f(0)>c·g(0) for every c>0. Hence no O witness with threshold N=0 exists; N=1 excludes this finite prefix. This is what the MKO means by finite prefixes being absorbed into the witness. S08 · impliesBefore f(n)-3g(n)=5n+2 After f(n)\ge 3\,g(n)\ \forall n\ge 0\ \Rightarrow\ f\in\Omega(g)\ \text{with}\ (c,N)=(3,0) Conditions: n\ge 0 Rule: exists_intro · Uses: S01, mko_asymptotic_def Leaf basis: exists_intro + order_basics + def_unfold Unfold Ω: we need c>0 and N with f(n)≥c·g(n) for n≥N. Compute f(n)−3n²=5n+2, which is at least 2>0 for n≥0, so f(n)≥3g(n) for all n≥0. Taking c=3 and N=0 gives f∈Ω(g). The lower-bound witness can start at 0 because g(0)=0 is no obstacle. S09 · impliesBefore f\in O(g),\ f\in\Omega(g) After f\in\Theta(g)=\Theta(n^2) Conditions: none Rule: and_intro_elim · Uses: S06, S08, mko_asymptotic_def Leaf basis: and_intro_elim + mko_asymptotic_def By the MKO definition, Θ requires both O and Ω. These were proved in S06 and S08, so f∈Θ(n²). The two witnesses need not coincide: the upper bound uses (10,1) and the lower bound uses (3,0). S10 · impliesBefore 4n^2-f(n)=n^2-5n-2=n(n-5)-2 After n\ge 6\Rightarrow 4n^2-f(n)\ge 4>0;\quad n=5:\ f(5)=102>100=4\cdot 25 Conditions: n\ge 6 Rule: exists_intro · Uses: S02 Leaf basis: exists_intro + order_basics + distributive Another witness: c=4, N=6. 4n²−f(n)=n²−5n−2=n(n−5)−2 (N4 checks the identity). Sub-step S10.1 proves it is at least 4 for n≥6. So (4,6) is also an O witness. But at n=5, f(5)=102>100: a smaller c needs a larger N. Witnesses are not unique, and finitely many exceptions are absorbed by N. S11 · impliesBefore f(n)-3n^2=5n+2>0\ \forall n After \neg\exists N\ \forall n\ge N,\ f(n)\le 3\,g(n) Conditions: none Rule: quantifier_negation · Uses: S08 Leaf basis: quantifier_negation + order_basics For every n, f(n)−3n²=5n+2≥2>0, so f(n)≤3g(n) never holds. However large N is, n=N is a counterexample, so c=3 cannot serve as the O constant. The definition asks for some c, not every c; constant factors are absorbed into the witness, but not arbitrarily small ones. S12 · impliesBefore \text{assume}\ \exists c>0\ \exists N\ \forall n\ge N,\ f(n)\le c\,n After \text{contradiction, so}\ f\notin O(h) Conditions: none Rule: contradiction · Uses: S02, G3 Leaf basis: contradiction + archimedean + order_basics By contradiction: suppose a witness (c,N) gives f(n)≤c·n for n≥N. S12.1 constructs an n with n≥N and n>c; S12.2 shows this n satisfies f(n)>c·n, contradicting the assumption. So no witness exists and f∉O(n). S13 · impliesBefore f(n)\ge 5n\ge n\ (n\ge 0),\ f\notin O(h) After f\in\Omega(n),\ f\notin O(n),\ f\notin\Theta(n) Conditions: none Rule: and_intro_elim · Uses: S12, S01, mko_asymptotic_def Leaf basis: and_intro_elim + exists_intro + order_basics For n≥0, f(n)=3n²+5n+2≥5n≥n, so (c,N)=(1,0) is an Ω(n) witness and f∈Ω(n). But S12 showed f∉O(n). Θ(n) needs both, so f∉Θ(n). This shows that O, Ω and Θ are not interchangeable: the same f has n as a lower bound but not as an upper bound. ## Substeps and lemmas S03.1 · impliesBefore n\ge 1 After n^2-n=n(n-1)\ge 0,\ \text{so}\ n\le n^2 Conditions: n\ge 1 Rule: order_basics · Uses: order_basics, distributive Leaf basis: order_basics + distributive + add_inverse n≥1 gives n−1≥0 and n≥0. The product of two nonnegative numbers is nonnegative (multiply 0≤n−1 by n≥0), so n(n−1)≥0. By distributivity n(n−1)=n²−n, so n²−n≥0, and adding n to both sides gives n≤n². S03.2 · impliesBefore 1\le n,\ n\le n^2 After 1\le n\le n^2 Conditions: none Rule: order_basics · Uses: S03.1, order_basics Leaf basis: order_basics Chain the hypothesis 1≤n with n≤n² from S03.1; transitivity gives 1≤n≤n², in particular 1≤n². S03.1 and S03.2 together prove L_n_le_nsq. S10.1 · impliesBefore n\ge 6 After n-5\ge 1,\ n(n-5)\ge n\ge 6,\ n(n-5)-2\ge 4 Conditions: n\ge 6 Rule: order_basics · Uses: order_basics Leaf basis: order_basics n≥6 gives n−5≥1. Multiplying n−5≥1 by the positive number n gives n(n−5)≥n≥6. Subtracting 2 gives n(n−5)−2≥4>0. S12.1 · impliesBefore c>0,\ N\in\mathbb{N} After n=\max(n_0,N,1)\ \text{with}\ n_0>c:\ n\ge N,\ n>c,\ n\ge 1 Conditions: none Rule: archimedean · Uses: archimedean Leaf basis: archimedean + order_basics By the Archimedean property there is a natural number n0>c. Let n=max(n0,N,1); then n≥N, n≥n0>c, and n≥1>0. S12.2 · impliesBefore n>c,\ n\ge 1 After f(n)\ge 3n^2\ge n^2=n\cdot n>c\cdot n Conditions: none Rule: order_basics · Uses: S12.1, S03, order_basics Leaf basis: order_basics + square_nonneg f(n)=3n²+5n+2≥3n²≥n² (since 5n+2≥0 and 2n²≥0). Multiplying cc·n. But n≥N, so the assumption gives f(n)≤c·n, a contradiction. ## Reverse audits - S13 · premise_audit · S12, mko_asymptotic_def, and_intro_elim — f∉Θ(n) follows because one conjunct fails; f∈Ω(n) has an explicit witness. - S12.2 · premise_audit · S12.1, order_basics — The key is that the multiplier n is positive (n≥1); N9 gives one numeric illustration with c=50, n=51, which is only an example. - S12.1 · premise_audit · archimedean, order_basics — n depends on c and N, which is allowed in the contradiction: we only need one counterexample point for the given witness. - S12 · premise_audit · S02, contradiction, archimedean — The argument handles an arbitrary (c,N), so it refutes the existential statement itself, not just one witness pair. - S11 · premise_audit · S08, quantifier_negation — This refutes only c=3, not f∈O(g), which was proved with c=10. - S10.1 · premise_audit · order_basics — The multiplier n is positive; the conclusion holds for every n≥6 without relying on numeric checks. - S10 · premise_audit · S02, exists_intro, order_basics — The full tail is guaranteed by the proof in S10.1; N6, which checks n from 6 to 60, is a finite observation only and does not replace the proof. - S09 · sufficient_goal_reduction · S06, S08, and_intro_elim, mko_asymptotic_def — Goal Θ; by definition the conjunction of O and Ω is necessary and sufficient, and both were proved forwards. - S08 · premise_audit · mko_asymptotic_def, exists_intro, order_basics — It needs 5n+2≥0, which follows from n≥0 (N3 checks the difference as a polynomial identity). - S07 · premise_audit · G2, numeric_evaluation — This is an exact computation at one point (N2), valid for every c because the right side is 0. It does not affect the conclusion f∈O(g). - S06 · sufficient_goal_reduction · S02, S05, exists_intro, forall_intro — Goal f∈O(g); a sufficient condition is one full-tail witness pair, proved forwards in S05. - S05 · premise_audit · S04, order_basics, distributive — Adding requires each inequality to hold at the same n in the same direction; the claim is only for n≥1. - S04 · premise_audit · S03, order_basics — It needs a positive multiplier; multiplying by a negative number would reverse the direction. - S03.2 · premise_audit · S03.1, order_basics — Only transitivity of order is used. - S03.1 · premise_audit · order_basics, distributive — The multiplication rule for order needs a nonnegative multiplier; here n≥0. - S03 · premise_audit · L_n_le_nsq — It needs n≥1; at n=0, 1≤n² fails (0²=0), which is exactly why the threshold cannot be 0 in S07. - S02 · inverse_equivalence · mko_asymptotic_def, def_unfold — Unfolding and folding the definition are inverse moves. For n≥1, replacing the uniform constant by a c that may depend on n allows the pointwise choice c=f(n)/g(n), which provides no uniform tail bound. At n=0 even a pointwise bound fails because g(0)=0 and f(0)=2. - S01 · premise_audit · G1, G2, square_nonneg, order_basics — Nonnegativity is a precondition for using the definitions of O, Ω, Θ; a different cost model would give a different f, which is outside this comparison. ## Error controls and negative controls Finite benchmarks do not prove asymptotic relationsThe misconception identified in the MKO is proving an asymptotic relation from a few benchmark points. n²≤100n holds for n=1 to 100 (N7, a finite check), which looks like n²∈O(n); but at n=101, 10201>10100 (N8), and the argument of S12 (with f replaced by n²) proves n²∉O(n). Finite observations can suggest, never prove, a full-tail property. O, Ω and Θ are not interchangeablef∈Ω(n) but f∉O(n), so f∉Θ(n) (S13). Saying 'f is Θ(n²)' instead of 'f is O(n²)' requires a separate lower-bound proof (S08); using Ω as if it were O mistakes a lower bound for an upper bound. Big O is not an equationO(g) is a set of functions and f∈O(g) is membership. n∈O(n²) (from n≤n² in S03) and n²∈O(n²), yet n≠n²; treating f=O(g) as an equation and manipulating or reversing it is wrong. - f(n)>3n² for every n, so f∉O(n²) → reject — The definition needs only some c; c=10, N=1 works (S06). - f∈O(n²) can be witnessed with threshold N=0 → reject — f(0)=2>0=c·0 for every c>0, so N=0 is impossible. - n²≤100n for n=1 to 100, so n²∈O(n) → reject — At n=101, 10201>10100; the argument of S12 proves n²∉O(n). - f∈Ω(n), so f∈Θ(n) → reject — Θ also needs f∈O(n), and S12 proves f∉O(n). ## Result and limitations Under the declared cost model, f(n)=3n²+5n+2 satisfies f∈O(n²) (witness (10,1), or (4,6)) and f∈Ω(n²) (witness (3,0)), so f∈Θ(n²). Neither the threshold N=0 nor the constant c=3 can serve in an O witness. f∈Ω(n) but f∉O(n), so f∉Θ(n). - The general statement in MKO paragraph 2 (the Θ degree of a polynomial with nonnegative coefficients is its highest nonzero degree) is not proved in general here; this guide treats one explicit quadratic. The binding to standard asymptotic predicates and the eventually filter (MKO formal next) is not built. ## Verification and source binding 9 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 7a11383e169a5fc2b0f70944b4267fe3da8b99b70a214469a16c5494bb46cd15 - original source SHA-256: 7a11383e169a5fc2b0f70944b4267fe3da8b99b70a214469a16c5494bb46cd15 - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-asymptotic-resource-bound-01.json)