漸近資源界：證明 3n²+5n+2∈Θ(n²) 並排除 Θ(n)

目標與範圍

設成本函數 f(n)=3n²+5n+2（n 從 0 起），比較函數 g(n)=n² 與 h(n)=n。以明示的全尾段 witness 證明 f∈O(g)（c=10、N=1）、f∈Ω(g)（c=3、N=0），故 f∈Θ(g)；說明 N=0 對 O 不可行、c=3 對 O 不可行、另一組 witness c=4、N=6 也可行；再證明 f∉O(h)，因此 f∈Ω(h) 但 f∉Θ(h)。

在 MKO 範圍內工作：n 為從 0 起的自然數，函數族與非負係數由題目明示（假設 a1）；每個漸近結論都給出全尾段 witness 並證明，有限數值核對只作觀察（假設 a2）。輸入大小與成本模型視為 f 的宣告的一部分；不討論特定算法如何得到 f，不使用一般多項式定理，不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• distributive
• numeric_evaluation
• archimedean
• square_nonneg

• G1 — 輸入大小 n 取遍從 0 起的自然數（MKO 假設 a1）。
• G2 — 成本函數 f(n)=3n²+5n+2 由題目宣告：它是在一個已固定的成本模型與輸入大小下，所計的基本操作數；係數 3、5、2 非負。
• G3 — 比較函數 g(n)=n² 與 h(n)=n。

• f(n)=3n^2+5n+2 — 宣告的成本函數
• g(n)=n^2,\ h(n)=n — 比較函數
• O(g),\ \Omega(g),\ \Theta(g) — 上界、下界、同階的函數集合
• (c,N) — witness：常數 c>0 與門檻 N
• n\ge N — 全尾段：所有不小於 N 的 n

規則與來源

• order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• archimedean · prerequisite — 阿基米德性質：對任意實數 x，存在自然數 n>x；因此對任意 ε>0，存在 n 使 1/n<ε。
• square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• mko_asymptotic_def · cited — 對非負函數 f,g:N→R，f∈O(g) 表示存在 c>0、N，使所有 n≥N 均有 f(n)≤c·g(n)；f∈Ω(g) 表示存在 c>0、N，使所有 n≥N 均有 f(n)≥c·g(n)；f∈Θ(g) 表示兩者同時成立。輸入大小與成本模型是聲明的一部分。 · mko-asymptotic-resource-bound
• L_n_le_nsq · lemma — 對每個自然數 n≥1：1≤n≤n²。

逐步主鏈

f(n)=3n^2+5n+2,\ g(n)=n^2,\ h(n)=n

f(n)>0,\ g(n)\ge 0,\ h(n)\ge 0\ \text{for all}\ n\ge 0

f\in O(g)

\exists c>0\ \exists N\in\mathbb{N}\ \forall n\ge N,\ f(n)\le c\,g(n)

n\in\mathbb{N},\ n\ge 1

1\le n\le n^2

n\le n^2,\ 1\le n^2\ (n\ge 1)

5n\le 5n^2,\ 2\le 2n^2\ (n\ge 1)

f(n)=3n^2+5n+2

f(n)\le 3n^2+5n^2+2n^2=10n^2\quad(n\ge 1)

\forall n\ge 1,\ f(n)\le 10\,g(n)

f\in O(g)\ \text{with witness}\ (c,N)=(10,1)

n=0

f(0)=2>0=c\cdot g(0)\ \text{for every}\ c>0

f(n)-3g(n)=5n+2

f(n)\ge 3\,g(n)\ \forall n\ge 0\ \Rightarrow\ f\in\Omega(g)\ \text{with}\ (c,N)=(3,0)

f\in O(g),\ f\in\Omega(g)

f\in\Theta(g)=\Theta(n^2)

4n^2-f(n)=n^2-5n-2=n(n-5)-2

n\ge 6\Rightarrow 4n^2-f(n)\ge 4>0;\quad n=5:\ f(5)=102>100=4\cdot 25

f(n)-3n^2=5n+2>0\ \forall n

\neg\exists N\ \forall n\ge N,\ f(n)\le 3\,g(n)

\text{assume}\ \exists c>0\ \exists N\ \forall n\ge N,\ f(n)\le c\,n

\text{contradiction, so}\ f\notin O(h)

f(n)\ge 5n\ge n\ (n\ge 0),\ f\notin O(h)

f\in\Omega(n),\ f\notin O(n),\ f\notin\Theta(n)

局部子步與引理

n\ge 1

n^2-n=n(n-1)\ge 0,\ \text{so}\ n\le n^2

1\le n,\ n\le n^2

1\le n\le n^2

n\ge 6

n-5\ge 1,\ n(n-5)\ge n\ge 6,\ n(n-5)-2\ge 4

c>0,\ N\in\mathbb{N}

n=\max(n_0,N,1)\ \text{with}\ n_0>c:\ n\ge N,\ n>c,\ n\ge 1

n>c,\ n\ge 1

f(n)\ge 3n^2\ge n^2=n\cdot n>c\cdot n

逐步反向審查

• S13 · premise_audit · S12, mko_asymptotic_def, and_intro_elim — f∉Θ(n) 由合取的一部分不成立得到；f∈Ω(n) 有明示 witness。
• S12.2 · premise_audit · S12.1, order_basics — 關鍵是乘數 n 為正（n≥1）；N9 以 c=50、n=51 作一個數值例示，只是例子。
• S12.1 · premise_audit · archimedean, order_basics — n 依賴於 c 與 N，這在反證中是允許的：我們只需對給定的 witness 找一個反例點。
• S12 · premise_audit · S02, contradiction, archimedean — 反證針對任意的 (c,N)，所以否定的是存在命題本身，不只是某一組 witness。
• S11 · premise_audit · S08, quantifier_negation — 這只否定 c=3，不否定 f∈O(g)，後者已由 c=10 證得。
• S10.1 · premise_audit · order_basics — 乘數 n 為正；結論對每個 n≥6 都成立，不依賴數值核對。
• S10 · premise_audit · S02, exists_intro, order_basics — 全尾段由 S10.1 的證明保證；N6 在 6 到 60 上的核對只是有限觀察，不取代證明。
• S09 · sufficient_goal_reduction · S06, S08, and_intro_elim, mko_asymptotic_def — 目標 Θ；依定義充要條件是 O 與 Ω 的合取，兩者都已正向證明。
• S08 · premise_audit · mko_asymptotic_def, exists_intro, order_basics — 需要 5n+2≥0，由 n≥0 得到（N3 以多項式恆等式核對差式）。
• S07 · premise_audit · G2, numeric_evaluation — 這是一個點的精確計算（N2），對所有 c 都成立因為右邊是 0。它不影響 f∈O(g) 的結論。
• S06 · sufficient_goal_reduction · S02, S05, exists_intro, forall_intro — 目標 f∈O(g)；足夠條件是找到一對全尾段 witness，由 S05 正向證得。
• S05 · premise_audit · S04, order_basics, distributive — 相加需要每個不等式都在同一個 n 上、同一方向成立；只對 n≥1 宣稱。
• S04 · premise_audit · S03, order_basics — 需要乘數為正；若乘以負數方向會反轉。
• S03.2 · premise_audit · S03.1, order_basics — 只用到次序的傳遞。
• S03.1 · premise_audit · order_basics, distributive — 次序的乘法規則需要乘數非負；這裡 n≥0。
• S03 · premise_audit · L_n_le_nsq — 需要 n≥1；n=0 時 1≤n² 不成立（0²=0），這正是 S07 中門檻不能取 0 的原因。
• S02 · inverse_equivalence · mko_asymptotic_def, def_unfold — 展開與折回定義互為反向。在 n≥1 的範圍，若改成『對每個 n 存在可依 n 改變的 c』，可逐點取 c=f(n)/g(n)，這不提供統一的尾段界；n=0 則因 g(0)=0、f(0)=2，連逐點界也失敗。
• S01 · premise_audit · G1, G2, square_nonneg, order_basics — 非負性是使用 O、Ω、Θ 定義的前提；不同成本模型會給出不同的 f，不在本稿比較範圍。

錯誤控制與反例

有限 benchmark 不證明漸近關係

MKO 指出的誤解是用幾個 benchmark 點證明漸近關係。n²≤100n 在 n=1 到 100 都成立（N7，有限核對），看起來像 n²∈O(n)；但 n=101 時 10201>10100（N8），而 S12 的論證（把 f 換成 n²）證明 n²∉O(n)。有限觀察只能提示，不能證明全尾段性質。

O、Ω、Θ 不可互換

f∈Ω(n) 但 f∉O(n)，所以 f∉Θ(n)（S13）。把「f 是 O(n²)」說成「f 是 Θ(n²)」需要另外證明下界（S08）；把 Ω 當 O 用會把下界誤當上界。

大 O 不是等號

O(g) 是一個函數集合，f∈O(g) 是成員關係。n∈O(n²)（由 S03 的 n≤n²）且 n²∈O(n²)，但 n≠n²；把 f=O(g) 當等式而在兩邊做代數運算或反向閱讀都是錯的。

• 對每個 n 都有 f(n)>3n²，所以 f∉O(n²) → reject — 定義只需要某個 c；c=10、N=1 可行（S06）。
• f∈O(n²) 可以取門檻 N=0 → reject — f(0)=2>0=c·0 對每個 c>0 都成立，N=0 不可能。
• n²≤100n 對 n=1 到 100 都成立，所以 n²∈O(n) → reject — n=101 時 10201>10100；S12 的論證證明 n²∉O(n)。
• f∈Ω(n)，所以 f∈Θ(n) → reject — Θ 還需要 f∈O(n)，而 S12 證明 f∉O(n)。

結論與限制

在宣告的成本模型下，f(n)=3n²+5n+2 滿足 f∈O(n²)（witness (10,1)，或 (4,6)）與 f∈Ω(n²)（witness (3,0)），所以 f∈Θ(n²)。門檻 N=0 與常數 c=3 都不能作為 O 的 witness。f∈Ω(n) 但 f∉O(n)，所以 f∉Θ(n)。

• MKO 第二段的一般敘述（非負係數多項式的 Θ 次數由最高非零次決定）未在此一般地證明；本稿只處理一個明示的二次式。與標準 asymptotic predicates 及 eventually filter 的綁定（MKO formal next）未建立。

驗證及來源綁定

9 個本稿宣告算術檢查；只支持所列算式。

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 7a11383e169a5fc2b0f70944b4267fe3da8b99b70a214469a16c5494bb46cd15
• original source SHA-256: 7a11383e169a5fc2b0f70944b4267fe3da8b99b70a214469a16c5494bb46cd15
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）