# 漸近資源界：證明 3n²+5n+2∈Θ(n²) 並排除 Θ(n) [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-asymptotic-resource-bound/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-asymptotic-resource-bound-01 · production-20261019-adopted-96 ## 目標與範圍 設成本函數 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 — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - 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²。 ## 逐步主鏈 S01 · definition操作前 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 條件：n\in\mathbb{N} 規則：def_intro · 依賴：G1, G2, G3 葉節點依據：def_intro + square_nonneg + order_basics 命名三個函數並確認 MKO 要求的非負性：n≥0 時 n²≥0，所以 3n²≥0、5n≥0，再加上 2>0 得 f(n)>0；g(n)=n²≥0；h(n)=n≥0。成本模型與輸入大小已隨 f 宣告（G2），之後只比較這個宣告下的函數。 S02 · equivalent操作前 f\in O(g) 操作後 \exists c>0\ \exists N\in\mathbb{N}\ \forall n\ge N,\ f(n)\le c\,g(n) 條件：無 規則：def_unfold · 依賴：S01, mko_asymptotic_def 葉節點依據：def_unfold + mko_asymptotic_def 展開大 O 的定義：要找到一對 witness (c,N)，使從 N 起的整個尾段都滿足 f(n)≤c·g(n)。量詞順序是「存在 c、N，對所有 n」：c 與 N 不可依賴 n。Ω 的定義把 ≤ 換成 ≥，Θ 要求兩者都成立。 S03 · theorem_application操作前 n\in\mathbb{N},\ n\ge 1 操作後 1\le n\le n^2 條件：n\ge 1 規則：L_n_le_nsq · 依賴：G1 葉節點依據：order_basics + distributive 套用引理 L_n_le_nsq（在 S03.1、S03.2 證明）：n≥1 時 1≤n≤n²。這讓低次項 5n 與常數 2 都能用 n² 控制。 S04 · implies操作前 n\le n^2,\ 1\le n^2\ (n\ge 1) 操作後 5n\le 5n^2,\ 2\le 2n^2\ (n\ge 1) 條件：n\ge 1; 5>0,\ 2>0 規則：order_basics · 依賴：S03 葉節點依據：order_basics 把 n≤n² 兩邊乘以正數 5，把 1≤n² 兩邊乘以正數 2；乘以正數保持不等式方向。 S05 · implies操作前 f(n)=3n^2+5n+2 操作後 f(n)\le 3n^2+5n^2+2n^2=10n^2\quad(n\ge 1) 條件：n\ge 1 規則：order_basics · 依賴：S04 葉節點依據：order_basics + distributive + add_assoc 把 S04 的兩個不等式與 3n²=3n² 相加（不等式同向相加），得 f(n)≤10n²，對每個 n≥1 成立。等價地，10n²−f(n)=5n(n−1)+2(n²−1)，兩項在 n≥1 時都非負（N1 以多項式恆等式核對）。 S06 · implies操作前 \forall n\ge 1,\ f(n)\le 10\,g(n) 操作後 f\in O(g)\ \text{with witness}\ (c,N)=(10,1) 條件：10>0 規則：exists_intro · 依賴：S05, S02 葉節點依據：exists_intro + forall_intro S05 對任意 n≥1 證明，沒有額外假設，所以依全稱推廣對整個尾段 n≥1 成立。取 c=10>0、N=1，依 ∃引入與 S02 的等價，f∈O(g)。 S07 · implies操作前 n=0 操作後 f(0)=2>0=c\cdot g(0)\ \text{for every}\ c>0 條件：無 規則：numeric_evaluation · 依賴：G2, G3 葉節點依據：numeric_evaluation + mul_zero 門檻的作用：f(0)=2，而 g(0)=0，所以對任何 c>0 都有 f(0)>c·g(0)。因此任何以 N=0 為門檻的 O witness 都不存在；N=1 把這個有限前綴排除在外。MKO 所說「有限前綴被吸收到 witness 中」就是這個意思。 S08 · implies操作前 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) 條件：n\ge 0 規則：exists_intro · 依賴：S01, mko_asymptotic_def 葉節點依據：exists_intro + order_basics + def_unfold 展開 Ω：需要 c>0、N 使 n≥N 時 f(n)≥c·g(n)。計算 f(n)−3n²=5n+2，n≥0 時它 ≥2>0，所以 f(n)≥3g(n) 對所有 n≥0 成立。取 c=3、N=0，得 f∈Ω(g)。下界的 witness 可以從 0 起，因為 g(0)=0 不構成障礙。 S09 · implies操作前 f\in O(g),\ f\in\Omega(g) 操作後 f\in\Theta(g)=\Theta(n^2) 條件：無 規則：and_intro_elim · 依賴：S06, S08, mko_asymptotic_def 葉節點依據：and_intro_elim + mko_asymptotic_def 依 MKO 定義，Θ 要求 O 與 Ω 同時成立。兩者分別由 S06 與 S08 證得，所以 f∈Θ(n²)。兩個 witness 不必相同：上界用 (10,1)，下界用 (3,0)。 S10 · implies操作前 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 條件：n\ge 6 規則：exists_intro · 依賴：S02 葉節點依據：exists_intro + order_basics + distributive 另一組 witness：c=4、N=6。4n²−f(n)=n²−5n−2=n(n−5)−2（N4 核對恆等式）。子步 S10.1 證明 n≥6 時它 ≥4。所以 (4,6) 也是 O 的 witness。但 n=5 時 f(5)=102>100：用較小的 c，就需要較大的 N。witness 不唯一，有限個例外點由 N 吸收。 S11 · implies操作前 f(n)-3n^2=5n+2>0\ \forall n 操作後 \neg\exists N\ \forall n\ge N,\ f(n)\le 3\,g(n) 條件：無 規則：quantifier_negation · 依賴：S08 葉節點依據：quantifier_negation + order_basics 對每個 n，f(n)−3n²=5n+2≥2>0，所以 f(n)≤3g(n) 從不成立。無論 N 取多大，n=N 就是反例，所以 c=3 不能作為 O 的常數。定義只要求「存在某個 c」，不是「每個 c 都行」；常數因子要由 witness 吸收，但不能任意小。 S12 · implies操作前 \text{assume}\ \exists c>0\ \exists N\ \forall n\ge N,\ f(n)\le c\,n 操作後 \text{contradiction, so}\ f\notin O(h) 條件：無 規則：contradiction · 依賴：S02, G3 葉節點依據：contradiction + archimedean + order_basics 反證：假設有 witness (c,N) 使 n≥N 時 f(n)≤c·n。S12.1 構造一個 n≥N 且 n>c；S12.2 證明此 n 滿足 f(n)>c·n，與假設矛盾。所以沒有任何 witness，f∉O(n)。 S13 · implies操作前 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) 條件：無 規則：and_intro_elim · 依賴：S12, S01, mko_asymptotic_def 葉節點依據：and_intro_elim + exists_intro + order_basics n≥0 時 f(n)=3n²+5n+2≥5n≥n，所以 (c,N)=(1,0) 是 Ω(n) 的 witness，f∈Ω(n)。但 S12 已證 f∉O(n)。Θ(n) 要求兩者兼具，所以 f∉Θ(n)。這說明 O、Ω、Θ 不能互換：同一個 f 對 n 有下界卻沒有上界。 ## 局部子步與引理 S03.1 · implies操作前 n\ge 1 操作後 n^2-n=n(n-1)\ge 0,\ \text{so}\ n\le n^2 條件：n\ge 1 規則：order_basics · 依賴：order_basics, distributive 葉節點依據：order_basics + distributive + add_inverse n≥1 給出 n−1≥0 且 n≥0。兩個非負數相乘仍非負（由 0≤n−1 乘以 n≥0），所以 n(n−1)≥0。依分配律 n(n−1)=n²−n，故 n²−n≥0，兩邊加 n 得 n≤n²。 S03.2 · implies操作前 1\le n,\ n\le n^2 操作後 1\le n\le n^2 條件：無 規則：order_basics · 依賴：S03.1, order_basics 葉節點依據：order_basics 把假設 1≤n 與 S03.1 的 n≤n² 串起來，依傳遞得 1≤n≤n²，特別地 1≤n²。S03.1 與 S03.2 合起來證得 L_n_le_nsq。 S10.1 · implies操作前 n\ge 6 操作後 n-5\ge 1,\ n(n-5)\ge n\ge 6,\ n(n-5)-2\ge 4 條件：n\ge 6 規則：order_basics · 依賴：order_basics 葉節點依據：order_basics n≥6 給出 n−5≥1。把 n−5≥1 兩邊乘以正數 n，得 n(n−5)≥n≥6。兩邊減 2，得 n(n−5)−2≥4>0。 S12.1 · implies操作前 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 條件：無 規則：archimedean · 依賴：archimedean 葉節點依據：archimedean + order_basics 依阿基米德性質，存在自然數 n0>c。令 n=max(n0,N,1)，則 n≥N、n≥n0>c，且 n≥1>0。 S12.2 · implies操作前 n>c,\ n\ge 1 操作後 f(n)\ge 3n^2\ge n^2=n\cdot n>c\cdot n 條件：無 規則：order_basics · 依賴：S12.1, S03, order_basics 葉節點依據：order_basics + square_nonneg f(n)=3n²+5n+2≥3n²≥n²（因 5n+2≥0 與 2n²≥0）。由 cc·n。但 n≥N，假設給 f(n)≤c·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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-asymptotic-resource-bound-01.json)