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

目標與範圍

對 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。

逐步主鏈

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)

f=[3,-4,6]

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

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

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

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]

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}

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

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

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

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

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

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

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

P=F_0+p_0

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

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

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}

5x^0,\ 0

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

p(x)=2x

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

\text{S05, S06, S09}

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

局部子步與引理

\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)

0<|h|\le 1

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

\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

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

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

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

逐步反向審查

• 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、反控制與修訂記錄）