# 原函數：多項式代表原函數、常數族與候選驗收

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-antiderivative/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-antiderivative-01 · production-20261019-adopted-96



## 目標與範圍

對 f=[3,−4,6]（f(x)=3−4x+6x²）：由定義證明四次以下多項式的求導公式；構造代表原函數 F0=[0,3,−2,2] 並驗證 F0'=f；證明 F0+C 對每個實數 C 都是原函數，且在至多五個係數的多項式中每個原函數都是 F0+C；驗收候選 G=[7,3,−2,2]（接受）、H=[0,3,−4,2]（拒絕）、K=[0,3,−3,8/3]（兩個測點相符仍拒絕）；求 F0(2)+C（C=−5），並說明原函數不是反函數。

只在 MKO 的全實數多項式模型內工作：f 的具體輸入至多四個整數係數，G、H、K 等驗收候選至多五個有理係數，均用升冪列表；一般原函數族 F0+C 與係數證明則容許實數 C 及實係數多項式。「只差常數」只在多項式模型內以係數證明；一般可微函數在區間上的版本需要平均值定理，不在本稿證明。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- distributive
- power_laws
- abs_rules
- order_basics
- frac_rules
- numeric_evaluation


- G1 — 多項式以升冪列表表示，論域為整個 ℝ（一個區間）；末端零正規化。
- G2 — f=[3,−4,6]。
- G3 — 候選 G=[7,3,−2,2]、H=[0,3,−4,2]、K=[0,3,−3,8/3]；求值資料 x=2、C=−5。


- [a_0,a_1,a_2,a_3] — 升冪係數列表
- F_0 — 常數項為 0 的代表原函數
- F_0+C — 原函數常數族
- D,\ R,\ M — 差商的主項、餘項與餘項的界





## 規則與來源


- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- 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。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- mko_antideriv · cited — F 是 f 在區間上的原函數，指 F 在該區間可微且 F'=f。全 ℝ 多項式 f(x)=Σa_k x^k 有代表 F0(x)=Σa_k x^(k+1)/(k+1)，常數項固定 0；F0+C 仍為原函數。多項式原函數的導數係數相同時，非零次係數相同，只差常數項。 · mko-antiderivative
- mko_derivative_def · cited — 對 f:ℝ→ℝ，f 在 x 的導數是 lim_(h→0,h≠0)(f(x+h)−f(x))/h，若此兩側有限極限存在。 · mko-derivative
- poly_coeff_identity · prerequisite — 兩個實係數多項式若在每個實數 x 取值相同，則正規化後的係數列表相同（非零多項式只有有限個根）。
- L_poly_deriv4 · lemma — 對 p(x)=c0+c1x+c2x²+c3x³+c4x⁴（實係數）與每個實數 x：p 在 x 可微且 p'(x)=c1+2c2x+3c3x²+4c4x³；即 [c0,c1,c2,c3,c4] 的導數列表為 [c1,2c2,3c3,4c4]。
- L_same_deriv · lemma — 若 P=[p0,p1,p2,p3,p4] 在 ℝ 上滿足 P'=f，則 p1=3、p2=−2、p3=2、p4=0，即 P=F0+p0。





## 逐步主鏈

S01 · definition操作前

F\ \text{antiderivative of}\ f\ \text{on}\ \mathbb{R}

操作後

F\ \text{differentiable on}\ \mathbb{R}\ \land\ \forall x\in\mathbb{R}:\ F'(x)=f(x)

條件：無

規則：mko_antideriv · 依賴：G1

葉節點依據：mko_antideriv + def_unfold

依 MKO：原函數 F 要在區間（這裡是整個 ℝ）可微，而且導函數處處等於 f。這是關於導數的條件，與「反函數」或「導數取倒數」無關。



S02 · equivalent操作前

f=[3,-4,6]

操作後

f(x)=3-4x+6x^2

條件：無

規則：def_unfold · 依賴：G2, G1

葉節點依據：def_unfold

升冪讀法：常數 3、x 的係數 −4、x² 的係數 6。



S03 · implies操作前

p=[c_0,c_1,c_2,c_3,c_4]

操作後

p'=[c_1,2c_2,3c_3,4c_4]\ \text{on}\ \mathbb{R}

條件：無

規則：L_poly_deriv4 · 依賴：mko_derivative_def

葉節點依據：mko_derivative_def + distributive + abs_rules + order_basics

依引理 L_poly_deriv4，四次以下多項式處處可微，導數列表是 [c1,2c2,3c3,4c4]；常數項 c0 不出現在導數中。引理由導數定義在 S03.1 至 S03.3 證明。本稿所有求導的多項式都至多四次。



S04 · definition操作前

a_k\ \mapsto\ \tfrac{a_k}{k+1}\ \text{as the coefficient of}\ x^{k+1}

操作後

F_0=[0,\ \tfrac31,\ \tfrac{-4}{2},\ \tfrac63]=[0,3,-2,2]

條件：無

規則：mko_antideriv · 依賴：S02, mko_antideriv

葉節點依據：mko_antideriv + frac_rules + numeric_evaluation

依 MKO 的代表公式：x^k 的係數 a_k 變成 x^(k+1) 的係數 a_k/(k+1)，常數項取 0。3/1=3、−4/2=−2、6/3=2（N4、N5），所以 F0=3x−2x²+2x³。係數以最簡分數寫出，分母為正。



S05 · implies操作前

F_0=[0,3,-2,2]

操作後

F_0'=[3,\ 2\cdot(-2),\ 3\cdot 2]=[3,-4,6]=f;\ F_0\ \text{is an antiderivative}

條件：無

規則：L_poly_deriv4 · 依賴：S03, S04, S02, S01

葉節點依據：L_poly_deriv4 + mko_antideriv + numeric_evaluation

依引理，F0 處處可微，導數列表 [3,−4,6]，即 3−4x+6x²=f(x)，對每個 x 成立（N6 為多項式恆等式）。依 S01，F0 是 f 在 ℝ 上的原函數。



S06 · implies操作前

F_0+C=[C,3,-2,2],\ C\in\mathbb{R}

操作後

(F_0+C)'=[3,-4,6]=f\ \text{for every}\ C

條件：無

規則：L_poly_deriv4 · 依賴：S03, S05

葉節點依據：L_poly_deriv4 + forall_intro

F0+C 的列表只在常數項不同；引理的導數列表不含 c0，所以導數仍是 [3,−4,6]=f。C 任意，依全稱推廣，整個常數族 F0+C 都是原函數。給出一個原函數 F0 與給出全部原函數不同。



S07 · implies操作前

G=[7,3,-2,2]

操作後

G=F_0+7,\ G'=f:\ \text{accept}

條件：無

規則：L_poly_deriv4 · 依賴：G3, S06

葉節點依據：L_poly_deriv4 + forall_elim

G 與 F0 只在常數項不同（7 對 0），所以 G=F0+7；由 S06 取 C=7，G'=f，接受。候選的常數項不影響驗收。



S08 · implies操作前

H=[0,3,-4,2]

操作後

H'=[3,-8,6]\neq[3,-4,6]=f:\ \text{reject}

條件：無

規則：L_poly_deriv4 · 依賴：G3, S03, S02

葉節點依據：L_poly_deriv4 + quantifier_negation + numeric_evaluation

依引理，H'=[3,2·(−4),3·2]=[3,−8,6]。索引 1 的係數（由 0 起算） −8≠−4，所以 H'−f=−4x，不是零多項式；例如 x=1 時 H'(1)=1、f(1)=5（N7、N8）。H 被拒絕。



S09 · implies操作前

P=[p_0,p_1,p_2,p_3,p_4],\ P'=f\ \text{on}\ \mathbb{R}

操作後

P=F_0+p_0

條件：無

規則：L_same_deriv · 依賴：S03, S04

葉節點依據：poly_coeff_identity + frac_rules + mul_inverse_nonzero

依引理 L_same_deriv，在至多五個係數的多項式中，任何原函數都與 F0 只差常數項。這正是 MKO 所說「導數係數相同時，非零次係數相同」。引理在 S09.1、S09.2 證明。



S10 · equivalent操作前

F_0(2)+C,\ C=-5

操作後

(3\cdot 2-2\cdot 2^2+2\cdot 2^3)+(-5)=14-5=9

條件：無

規則：numeric_evaluation · 依賴：S04, G3

葉節點依據：numeric_evaluation

F0(2)=6−8+16=14（N9），加 C=−5 得 9（N10）。求導會消去 C，但求值不會：C 與 x 都是真正的資料，不能因為導數不含 C 就把它刪掉。



S11 · implies操作前

K=[0,3,-3,\tfrac83]

操作後

K'=[3,-6,8];\ K'(0)=f(0),\ K'(1)=f(1),\ K'(2)=23\neq 19=f(2):\ \text{reject}

條件：無

規則：L_poly_deriv4 · 依賴：G3, S03, S02

葉節點依據：L_poly_deriv4 + quantifier_negation + numeric_evaluation

依引理，K'=[3,2·(−3),3·(8/3)]=[3,−6,8]。K'−f=2x²−2x=2x(x−1)（N14），在 x=0、x=1 恰為 0，所以只在這兩點抽樣會誤判（N11、N12）；但它不是零多項式，x=2 時 K'(2)=23、f(2)=19（N13）。逐係數比較（−6≠−4）直接拒絕 K。



S12 · implies操作前

5x^0,\ 0

操作後

5x^0=5\ (\text{also at}\ x=0)\ \to\ [0,5];\ 0\ \to\ [0]

條件：無

規則：mko_antideriv · 依賴：S03, mko_antideriv

葉節點依據：mko_antideriv + L_poly_deriv4 + power_laws

單項式邊界：在多項式中 x^0 恆為 1，包括 x=0，所以 5x^0 是常數 5，代表原函數為 5x，即 [0,5]（導數 [5]，由引理）。係數 c=0 時函數為零，代表原函數正規化為 [0]，不保留無意義的高次零項；其原函數族是所有常數。



S13 · implies操作前

p(x)=2x

操作後

\text{antiderivative}\ x^2;\ \text{inverse}\ y\mapsto\tfrac y2;\ 1/p'=\tfrac12:\ \text{three different objects}

條件：無

規則：mko_antideriv · 依賴：S03, S01

葉節點依據：mko_antideriv + L_poly_deriv4 + quantifier_negation

對 p(x)=2x：原函數 x²（[0,0,1]，由引理導數為 [0,2]=p）；反函數是 y↦y/2；導數的倒數是 1/2。在輸入 4，x² 給 16，反函數給 2（N15）。三者完全不同，原函數不是反函數，也不是導數取倒數。



S14 · implies操作前

\text{S05, S06, S09}

操作後

\{P:\ P'=f,\ P\ \text{at most five coefficients}\}=\{F_0+C:\ C\in\mathbb{R}\}

條件：無

規則：set_extensionality · 依賴：S05, S06, S09

葉節點依據：set_extensionality + subset_def

S06 給出 ⊇（每個 F0+C 都是原函數），S09 給出 ⊆（每個這樣的 P 都是 F0+p0）。依集合外延性，兩集合相等：在多項式模型中，f 的原函數恰是常數族 F0+C。







## 局部子步與引理

S03.1 · equivalent操作前

\frac{p(x+h)-p(x)}{h}\ (h\neq 0)

操作後

D+hR,\ D=c_1+2c_2x+3c_3x^2+4c_4x^3,\ R=c_2+c_3(3x+h)+c_4(6x^2+4xh+h^2)

條件：h\neq 0

規則：distributive · 依賴：distributive, power_laws, frac_rules

葉節點依據：distributive + power_laws + frac_rules + mul_inverse_nonzero

逐次方展開：(x+h)²−x²=h(2x+h)，(x+h)³−x³=h(3x²+h(3x+h))，(x+h)⁴−x⁴=h(4x³+h(6x²+4xh+h²))（N1、N2、N3）。乘上係數相加、c0 相消，得 p(x+h)−p(x)=h(D+hR)；h≠0 時除以 h。



S03.2 · implies操作前

0<|h|\le 1

操作後

|R|\le M=|c_2|+|c_3|(3|x|+1)+|c_4|(6x^2+4|x|+1)

條件：|h|\le 1

規則：abs_rules · 依賴：S03.1, abs_rules

葉節點依據：abs_rules + order_basics + square_nonneg

三角不等式與 |uv|=|u||v|，再用 |h|≤1、h²≤1：|3x+h|≤3|x|+1，|6x²+4xh+h²|≤6x²+4|x|+1。M 只依 x 與係數。



S03.3 · implies操作前

\varepsilon>0,\ \delta=\min\left(1,\tfrac{\varepsilon}{M+1}\right)

操作後

0<|h|<\delta\Rightarrow|(D+hR)-D|\le|h|M<\varepsilon;\ p'(x)=D

條件：M+1>0

規則：mko_derivative_def · 依賴：S03.1, S03.2, mko_derivative_def

葉節點依據：mko_derivative_def + forall_intro + order_basics + abs_rules

若 0<|h|<δ，則 |h|<1，S03.2 適用：|hR|≤|h|M≤|h|(M+1)<δ(M+1)≤ε。ε 任意，依導數定義 p'(x)=D。x 任意，所以處處可微。S03.1 至 S03.3 證得引理 L_poly_deriv4。



S09.1 · implies操作前

P'(x)=f(x)\ \forall x

操作後

[p_1,2p_2,3p_3,4p_4]=[3,-4,6,0]

條件：無

規則：poly_coeff_identity · 依賴：S03, S02, poly_coeff_identity

葉節點依據：poly_coeff_identity + def_unfold

由 S03，P' 的列表為 [p1,2p2,3p3,4p4]；f 補一個末端零為 [3,−4,6,0]（同一多項式）。兩者在每個 x 取值相同，依 poly_coeff_identity，係數逐項相同。



S09.2 · implies操作前

kp_k=a_{k-1}\ (k=1,2,3,4)

操作後

p_1=3,\ p_2=-2,\ p_3=2,\ p_4=0;\ P=[p_0,3,-2,2]=F_0+p_0

條件：k\neq 0

規則：frac_rules · 依賴：S09.1, frac_rules

葉節點依據：frac_rules + mul_inverse_nonzero + numeric_evaluation

k=1,2,3,4 都不為 0，可以除：p1=3/1=3，p2=−4/2=−2，p3=6/3=2，p4=0/4=0。所以 P 的非常數係數與 F0 完全相同，P=F0+p0，常數 p0 自由。S09.1、S09.2 證得引理 L_same_deriv。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S06, S09, set_extensionality — 目標 G：兩集合相等。足夠條件 H：雙向包含；H⇒G 由外延性。兩個包含分別由 S06、S09 正向證成。
- S13 · premise_audit · S03, S01 — 一個輸入的值不同就說明兩函數不同。
- S12 · premise_audit · S03, mko_antideriv — 依 MKO 假設 a2 的慣例；以引理核對導數。
- S11 · premise_audit · S03, quantifier_negation — 兩個相符的測點不能證明恆等；一個不符的係數或點就足以拒絕。
- S10 · inverse_equivalence · numeric_evaluation — 精確求值。
- S09.2 · premise_audit · S09.1, frac_rules, mul_inverse_nonzero — k=0 的位置（常數項）沒有方程，所以 p0 不受限制。
- S09.1 · premise_audit · S03, poly_coeff_identity — 從函數恆等到係數相等使用 poly_coeff_identity；僅像 S11 那樣核對兩個點仍不足以證明本題的恆等式。
- S09 · premise_audit · L_same_deriv — 結論限於多項式模型；不宣稱一般可微函數的區間版本。
- S08 · premise_audit · S03, quantifier_negation — 一點不等即可否定 H'=f。
- S07 · premise_audit · S06 — 逐係數比較 G 與 F0 的非常數項。
- S06 · premise_audit · S03, S05, forall_intro — 此步只證「F0+C 都是原函數」；「沒有其他」在 S09 證明。
- S05 · sufficient_goal_reduction · S01, S03, S04 — 目標 G：F0 是原函數。足夠條件 H：F0 可微且導數列表等於 f 的列表；H⇒G 由定義。H 由引理逐係數正向證成，沒有用有限測點。
- S04 · premise_audit · S02, mko_antideriv — 此步只依公式構造候選；是否為原函數由 S05 驗證。
- S03.3 · premise_audit · S03.1, S03.2, mko_derivative_def, forall_intro — 用 M+1 避免 M=0 時除以 0。
- S03.2 · premise_audit · abs_rules, order_basics — 只給上界；|h|≤1 由 S03.3 的 δ≤1 保證。
- S03.1 · inverse_equivalence · distributive, frac_rules — 恆等式加上 h≠0 時的除法，雙向成立。
- S03 · premise_audit · L_poly_deriv4, mko_derivative_def — 引理只涵蓋四次以下；候選至多五個係數，正好在範圍內。
- S02 · inverse_equivalence · def_unfold — 讀回列表得原列表。
- S01 · premise_audit · G1, mko_antideriv — 此步只寫出定義。





## 錯誤控制與反例

不要漏掉常數族MKO 的誤解之一是漏掉常數族。F0 只是選定的代表；全部原函數是 F0+C（S06、S14）。C 在求導時消失，但在求值時有作用：F0(2)+C 在 C=−5 時是 9，不是 14（S10）。

有限測點不能代替多項式恆等另一個誤解是以幾個相等測點代替 F'=f。K' 與 f 在 x=0、1 相等，因為差 2x(x−1) 在這兩點為零；但 x=2 時 23≠19（S11）。驗收要逐係數比較導數列表（S09.1 說明為何係數比較才對應函數恆等）。

原函數不是反函數第三個誤解是把原函數當反函數。p(x)=2x 的原函數是 x²，反函數是 y/2，導數的倒數是 1/2，三者不同（S13）。原函數的定義只涉及 F'=f（S01）。


- F0 是 f 唯一的原函數 → reject — F0+7=G 也是（S07）；全部原函數是 F0+C。
- K'(0)=f(0) 且 K'(1)=f(1)，所以 K 是原函數 → reject — K'(2)=23≠19=f(2)；K'=[3,−6,8]≠[3,−4,6]。
- 求導會消去 C，所以 C=−5 時 F0(2)+C=14 → reject — 求值保留 C：14+(−5)=9。
- 2x 的原函數是它的反函數 x/2 → reject — (x/2)'=1/2≠2x；原函數是 x²+C。
- 5x^0 在 x=0 是 0^0，所以它的原函數在 0 沒有定義 → reject — 多項式慣例 x^0=1（包括 x=0），5x^0 是常數 5，原函數 5x 處處有定義。





## 結論與限制

f=[3,−4,6] 的代表原函數是 F0=[0,3,−2,2]=3x−2x²+2x³，F0'=f。對每個實數 C，F0+C 都是原函數；在至多五個係數的多項式中，原函數恰是 F0+C。G=[7,3,−2,2]=F0+7 接受；H 因 H'=[3,−8,6] 拒絕；K′ 雖在 x=0、1 與 f 的值相符，但 K'=[3,−6,8]≠f，拒絕。F0(2)+C 在 C=−5 時為 9。原函數不是反函數，也不是導數的倒數。


- 一般可微函數在區間上「兩個原函數只差常數」需要平均值定理；本稿只在多項式模型內以係數證明，不外推到一般函數或不連通論域。
- poly_coeff_identity（處處相等的多項式係數相同）是本稿的前提，未在本稿中證明。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 0a7ad7b92f3eb8cf9c92f59c031efe93847f4df94d0f2541c2d6a9ae98227411
- original source SHA-256: 2ed700aa9d9c5a319e9f4d0ebcba193c2e7bdf4f88f31d9da27c9e22df7547ef
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-antiderivative-01.json)