# 定積分：以左端和的極限與矩公式計算 ∫₀³(x²−4)dx

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

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

derivation-mko-definite-integral-01 · production-20261019-adopted-96



## 目標與範圍

設 f(x)=x²−4、a=0、b=3。(1) 只用 Riemann 定義（所有合法標記分割和在網格趨 0 時的共同極限）與 f 可積的前提，由 N 等分左端和 L_N 的極限求出 I(f,0,3)；(2) 用本 MKO 明列的矩公式獨立再算一次並核對；(3) 求反向端點的 I(f,3,0)；(4) 以 N=3、N=50 說明有限左端和不等於積分，並說明有號積分不是非負面積。

只處理 MKO 範圍內的一個連續多項式 f(x)=x²−4（整數係數、次數 2）在有限區間 [0,3] 上的有號 Riemann 積分。f 的可積性取自 MKO 假設 a1，本稿不證明；本稿證明的是：在可積前提下，積分值必為 −3。不使用、也不宣稱證明一般微積分基本定理；不處理一般可積函數、Lebesgue 積分或面積理論；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- finite_sum_rules
- seq_limit_def
- archimedean
- order_basics
- numeric_evaluation


- G1 — f(x)=x²−4，端點 a=0≤b=3。f 是整數係數、次數 2 的多項式（升冪係數 −4、0、1），符合 MKO 假設 a1。
- G2 — MKO 假設 a1：f 在全 ℝ 連續，並在有限區間上可積；所以 I(f,0,3) 存在，是一個實數。
- G3 — MKO 假設 a3 的左端和：對 a≤b 與正整數 N，Δx=(b−a)/N，x_i=a+iΔx，L_N=Σ_{i=0}^{N−1} f(x_i)Δx。本例 Δx=3/N、x_i=3i/N。


- f(x)=x^2-4 — 被積多項式
- I(f,a,b) — f 從 a 到 b 的有向定積分
- N — 等分份數，正整數
- \Delta x=\tfrac{3}{N} — 每段長度，也是網格
- x_i=\tfrac{3i}{N} — 索引 i 的分點；0≤i<N 時也是第 i+1 段的左端標記
- L_N — N 等分左端和
- S(f,P,\xi) — 標記分割 (P,ξ) 的 Riemann 和





## 規則與來源


- finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。
- seq_limit_def · prerequisite — 數列極限：a_n→L 表示對每個 ε>0，存在 N 使所有 n≥N 都有 |a_n−L|<ε。
- archimedean · prerequisite — 阿基米德性質：對任意實數 x，存在自然數 n>x；因此對任意 ε>0，存在 n 使 1/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。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- 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）。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- 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。
- modus_ponens · prerequisite — 肯定前件：由 P 與 P⇒Q 得 Q。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_riemann_def · cited — 對有限實區間 a≤b 上的連續多項式 f，Riemann 定積分是所有合法標記分割和在網格趨 0 時的共同極限。 · mko-definite-integral
- mko_reverse · cited — 反向端點換號：I(f,a,b)=−I(f,b,a)；相同端點 I(f,a,a)=0。 · mko-definite-integral
- mko_moment · cited — 本切片明列矩公式 I(x^n,a,b)=(b^{n+1}−a^{n+1})/(n+1)；對 f=Σc_k x^k 逐係數相加：I(f,a,b)=Σc_k(b^{k+1}−a^{k+1})/(k+1)。 · mko-definite-integral
- riemann_limit_meaning · prerequisite — 「共同極限為 I」的精確意思：對每個 ε>0，存在 δ>0，使 [a,b] 的每個網格小於 δ 的標記分割 (P,ξ) 都有 |S(f,P,ξ)−I|<ε。分割 P 是有限嚴格遞增的分點 t_0=a<t_1<t_2 直到 t_m=b；標記 ξ_j 落在 [t_{j−1},t_j]；網格是最大的 t_j−t_{j−1}；S(f,P,ξ)=Σ_{j=1}^{m} f(ξ_j)(t_j−t_{j−1})。
- limit_unique · prerequisite — 數列極限唯一：若 s_N→L 且 s_N→L′，則 L=L′。
- L_sum_sq · lemma — 對每個正整數 N，Σ_{i=0}^{N−1} i²=(N−1)N(2N−1)/6。





## 逐步主鏈

S01 · definition操作前

I(f,0,3)

操作後

\forall\varepsilon>0\ \exists\delta>0:\ \operatorname{mesh}(P)<\delta\Rightarrow|S(f,P,\xi)-I(f,0,3)|<\varepsilon

條件：0\le 3

規則：mko_riemann_def · 依賴：G1, G2

葉節點依據：mko_riemann_def + riemann_limit_meaning + def_unfold

依 MKO 的定義，I(f,0,3) 是 [0,3] 上所有合法標記分割和在網格趨 0 時的共同極限；依 riemann_limit_meaning，這句話的精確意思是：對每個 ε>0 都有 δ>0，使每個網格小於 δ 的標記分割 (P,ξ) 都有 |S(f,P,ξ)−I(f,0,3)|<ε。G2 保證這樣的數存在；本稿的工作是求出它的值。



S02 · implies操作前

L_N=\sum_{i=0}^{N-1} f(x_i)\,\Delta x

操作後

L_N=S(f,P_N,\xi_N),\quad \operatorname{mesh}(P_N)=\tfrac{3}{N}

條件：N\ge 1

規則：riemann_limit_meaning · 依賴：G3, S01

葉節點依據：riemann_limit_meaning + order_basics + numeric_evaluation

取分點 x_i=3i/N（i=0 到 N）。相鄰兩點相差 3/N>0，所以分點嚴格遞增，且 x_0=0、x_N=3，構成 [0,3] 的分割 P_N。第 i+1 段 [x_i,x_{i+1}] 的標記取左端點 x_i，它確實落在該段內。每段長度都是 3/N，所以網格是 3/N。於是 L_N 正是一個合法的標記分割和。



S03 · implies操作前

\operatorname{mesh}(P_N)=\tfrac{3}{N}\ \text{and S01}

操作後

L_N\to I(f,0,3)\quad(N\to\infty)

條件：N\ge 1

規則：seq_limit_def · 依賴：S01, S02, archimedean

葉節點依據：seq_limit_def + archimedean + order_basics

給定 ε>0，取 S01 的 δ。依阿基米德性質取自然數 N_0>3/δ（且 N_0≥1）。對每個 N≥N_0，3/N≤3/N_0<δ，所以 P_N 的網格小於 δ，由 S01 得 |L_N−I(f,0,3)|<ε。這正是數列極限 L_N→I(f,0,3) 的定義。



S04 · equivalent操作前

f(x_i)\,\Delta x

操作後

\tfrac{27i^2}{N^3}-\tfrac{12}{N}

條件：N\ge 1

規則：distributive · 依賴：G1, G3

葉節點依據：distributive + frac_rules + power_laws

代入 x_i=3i/N：f(x_i)=(3i/N)²−4=9i²/N²−4；再乘 Δx=3/N，用分配律得 27i²/N³−12/N。



S05 · equivalent操作前

L_N=\sum_{i=0}^{N-1}\left(\tfrac{27i^2}{N^3}-\tfrac{12}{N}\right)

操作後

L_N=\tfrac{27}{N^3}\sum_{i=0}^{N-1} i^2-12

條件：N\ge 1

規則：finite_sum_rules · 依賴：S04, finite_sum_rules

葉節點依據：finite_sum_rules + frac_rules

有限和可逐項拆開，常數因子 27/N³ 可提出和號外；常數項 12/N 在 i=0 到 N−1 共出現 N 次，和為 N·(12/N)=12。



S06 · equivalent操作前

\sum_{i=0}^{N-1} i^2

操作後

\tfrac{(N-1)N(2N-1)}{6}

條件：N\ge 1

規則：L_sum_sq · 依賴：S05, L_sum_sq

葉節點依據：nat_induction + finite_sum_rules + distributive

依引理 L_sum_sq（在 S06.1 到 S06.3 證明）把平方和換成封閉式。



S07 · equivalent操作前

L_N=\tfrac{27}{N^3}\cdot\tfrac{(N-1)N(2N-1)}{6}-12

操作後

L_N=-3-\tfrac{27}{2N}+\tfrac{9}{2N^2}

條件：N\ge 1

規則：frac_rules · 依賴：S05, S06

葉節點依據：frac_rules + distributive + mul_inverse_nonzero

約分：27/N³·(N−1)N(2N−1)/6=9(N−1)(2N−1)/(2N²)=9(2N²−3N+1)/(2N²)=9−27/(2N)+9/(2N²)。再減 12 得 −3−27/(2N)+9/(2N²)。約去 N 需要 N≠0，由 N≥1 保證。



S08 · implies操作前

L_3,\ L_{50}

操作後

L_3=-7,\quad L_{50}=-\tfrac{16341}{5000}

條件：無

規則：numeric_evaluation · 依賴：S07, G3

葉節點依據：numeric_evaluation

N=3：Δx=1，左端點 0、1、2，f 值 −4、−3、0，直接相加得 L_3=−7；公式給 −3−27/6+9/18=−3−9/2+1/2=−7，一致。N=50（MKO 假設 a3 允許的最大 N）：L_50=−3−27/100+9/5000=−16341/5000=−3.2682。兩者都不等於 −3。



S09 · implies操作前

|L_N-(-3)|

操作後

\tfrac{27N-9}{2N^2}\le\tfrac{27}{2N}

條件：N\ge 1

規則：abs_rules · 依賴：S07

葉節點依據：abs_rules + order_basics + frac_rules

由 S07，L_N+3=−27/(2N)+9/(2N²)=−(27N−9)/(2N²)。N≥1 時 27N−9≥18>0，所以 |L_N+3|=(27N−9)/(2N²)。又 −9<0，故 (27N−9)/(2N²)≤27N/(2N²)=27/(2N)。



S10 · implies操作前

|L_N+3|\le\tfrac{27}{2N}\ \ (N\ge 1)

操作後

L_N\to -3

條件：\varepsilon>0

規則：seq_limit_def · 依賴：S09, archimedean

葉節點依據：seq_limit_def + archimedean + order_basics

給定 ε>0，依阿基米德性質取自然數 N_1>27/(2ε)。對每個 N≥N_1，|L_N−(−3)|≤27/(2N)≤27/(2N_1)<ε。依數列極限的定義，L_N→−3。



S11 · implies操作前

L_N\to I(f,0,3),\quad L_N\to -3

操作後

I(f,0,3)=-3

條件：無

規則：limit_unique · 依賴：S03, S10, limit_unique

葉節點依據：limit_unique + modus_ponens

同一個數列 L_N 既收斂到 I(f,0,3)（S03），又收斂到 −3（S10）；數列極限唯一，所以 I(f,0,3)=−3。



S12 · theorem_application操作前

I(f,0,3)=I(x^2,0,3)-4\,I(x^0,0,3)

操作後

\tfrac{3^3-0^3}{3}-4\cdot\tfrac{3^1-0^1}{1}=9-12=-3

條件：0\le 3

規則：mko_moment · 依賴：G1, mko_moment

葉節點依據：mko_moment + numeric_evaluation

第二條路：MKO 明列的矩公式逐係數相加。x² 的矩是 (3³−0³)/3=9，常數 1=x⁰ 的矩是 (3−0)/1=3，所以 I(f,0,3)=9−4·3=−3，與 S11 相同。



S13 · equivalent操作前

I(f,3,0)

操作後

-I(f,0,3)=3

條件：無

規則：mko_reverse · 依賴：S11, mko_reverse

葉節點依據：mko_reverse + neg_mul

反向端點要換號：I(f,3,0)=−I(f,0,3)=−(−3)=3。



S14 · theorem_application操作前

I(f,0,2),\ I(f,2,3)

操作後

-\tfrac{16}{3},\ \tfrac{7}{3}

條件：0\le 2; 2\le 3

規則：mko_moment · 依賴：G1, mko_moment

葉節點依據：mko_moment + numeric_evaluation + order_basics

用矩公式分段：I(f,0,2)=(2³−0)/3−4·2=8/3−8=−16/3；I(f,2,3)=(3³−2³)/3−4·(3−2)=19/3−4=7/3。兩段相加 −16/3+7/3=−3=I(f,0,3)。符號的來由：f(x)=(x−2)(x+2)，在 0≤x<2 時為負（例如 f(1)=−3），在 2<x≤3 時為正。



S15 · implies操作前

|I(f,0,3)|

操作後

3\neq\tfrac{23}{3}=|I(f,0,2)|+|I(f,2,3)|

條件：無

規則：numeric_evaluation · 依賴：S11, S14

葉節點依據：abs_rules + numeric_evaluation

有號積分讓負的一段與正的一段互相抵消：|I(f,0,3)|=3，而兩段絕對值之和是 16/3+7/3=23/3。所以「積分就是非負面積」或「取絕對值就得到積分」在這裡都不成立；MKO 假設 a2 明說積分是有向、有號的。



S16 · implies操作前

\text{goals (1) to (4)}

操作後

I(f,0,3)=-3,\ I(f,3,0)=3,\ L_3=-7,\ L_{50}=-\tfrac{16341}{5000}

條件：無

規則：and_intro_elim · 依賴：S08, S11, S12, S13, S15

葉節點依據：and_intro_elim

合併：(1) S11 由定義得 I(f,0,3)=−3；(2) S12 以矩公式得相同值；(3) S13 得 I(f,3,0)=3；(4) S08 顯示有限左端和不等於積分，S15 顯示有號積分不是非負面積。







## 局部子步與引理

S06.1 · induction_base操作前

\sum_{i=0}^{0} i^2

操作後

0=\tfrac{(1-1)\cdot 1\cdot(2\cdot 1-1)}{6}

條件：N=1

規則：numeric_evaluation · 依賴：finite_sum_rules

葉節點依據：finite_sum_rules + numeric_evaluation

N=1：和只有 i=0 一項，其值 0²=0；右邊 (1−1)·1·(2−1)/6=0。基礎情形成立。



S06.2 · induction_step操作前

\sum_{i=0}^{N-1} i^2=\tfrac{(N-1)N(2N-1)}{6}

操作後

\sum_{i=0}^{N} i^2=\tfrac{N(N+1)(2N+1)}{6}

條件：N\ge 1

規則：finite_sum_rules · 依賴：finite_sum_rules, distributive

葉節點依據：finite_sum_rules + distributive + add_comm

假設 N 的公式成立。新的和多了一項 i=N：Σ_{i=0}^{N} i²=(N−1)N(2N−1)/6+N²=N[(N−1)(2N−1)+6N]/6=N(2N²+3N+1)/6=N(N+1)(2N+1)/6。這正是把 N 換成 N+1 的公式，因為 (N+1)−1=N、2(N+1)−1=2N+1。



S06.3 · implies操作前

P(1)\ \land\ \forall N\ge 1\,(P(N)\Rightarrow P(N+1))

操作後

\forall N\ge 1:\ P(N)

條件：無

規則：nat_induction · 依賴：S06.1, S06.2, nat_induction

葉節點依據：nat_induction

令 P(N) 為「Σ_{i=0}^{N−1} i²=(N−1)N(2N−1)/6」。S06.1 給 P(1)，S06.2 給 P(N)⇒P(N+1)；依數學歸納原理（n₀=1），P(N) 對每個 N≥1 成立。S06.1 到 S06.3 合起來證得引理 L_sum_sq。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S08, S11, S12, S13, S15, and_intro_elim — 目標 G：四個小題。足夠條件 H：S08、S11、S12、S13、S15 的結論同時成立；H⇒G 只是合取。H 由 G1 到 G3 正向證成，沒有把 G 當作前提。
- S15 · premise_audit · S11, S14, abs_rules — 這是具體數字的比較（N15）。本稿不發展面積理論，23/3 只是兩段絕對值之和。
- S14 · premise_audit · mko_moment, numeric_evaluation, order_basics — 只是矩公式在兩段上的套用（N12 到 N14、N16）；不宣稱一般函數的區間可加性。
- S13 · inverse_equivalence · S11, mko_reverse — 再反向一次：I(f,0,3)=−I(f,3,0)=−3，回到 S11；換號規則兩向都成立。
- S12 · premise_audit · G1, mko_moment, numeric_evaluation — 矩公式是本切片明列的規則，此處只是套用；兩條路一致是互相核對。這不是一般微積分基本定理的證明，也不宣稱是。
- S11 · premise_audit · S03, S10, G2, limit_unique — 需要兩個極限屬於同一數列；S03 又依賴 G2 的存在性。若不知 f 可積，只能得到「左端和的極限是 −3」，不能稱為積分。
- S10 · premise_audit · S09, seq_limit_def, archimedean — 定義要求對所有 N≥N_1 成立，不只 N≤50；因此 S09 的上界必須對一般 N 證明，不能用有限表格代替。
- S09 · premise_audit · S07, abs_rules, order_basics — 需要 N≥1 才能確定 27N−9>0 並去掉絕對值；不等式只是單向上界，不宣稱相等。N10 在 N=1 到 50 做有限核對。
- S08 · premise_audit · S07, numeric_evaluation — 這是兩個 N 的數值（N5 到 N8），用來對照 S07 的公式並顯示有限和不是積分；它們不證明極限。
- S07 · inverse_equivalence · frac_rules, distributive, mul_inverse_nonzero — 兩邊同乘非零的 2N² 都化成同一個多項式 −6N²−27N+9（N3 為次數 2 的恆等式核對）；再除回 2N² 是允許的，所以雙向成立。N4 另在 N=1 到 50 逐點核對，那只是有限核對。
- S06.3 · premise_audit · S06.1, S06.2, nat_induction — 歸納原理需要基礎與歸納步兩者；兩者都已證，且證明中沒有使用引理本身。
- S06.2 · premise_audit · finite_sum_rules, distributive — 只用到 N 的歸納假設與多項式恆等式 (N−1)N(2N−1)/6+N²=N(N+1)(2N+1)/6（N1，次數 3 的格點恆等式核對）。
- S06.1 · premise_audit · finite_sum_rules, numeric_evaluation — 只需直接計算兩邊（N2）。
- S06 · inverse_equivalence · L_sum_sq — 兩式對每個 N≥1 相等，所以替換雙向成立。
- S05 · inverse_equivalence · finite_sum_rules, frac_rules — 反向：把 27/N³ 乘回每一項、把 12 寫成 N 個 12/N 之和，就回到原式；所用的有限和規則都是恆等式。
- S04 · inverse_equivalence · distributive, frac_rules, power_laws — 反向：提出公因子 3/N，得 (3/N)(9i²/N²−4)=f(x_i)Δx。N≠0 時兩式是同一個數。
- S03 · premise_audit · S01, S02, G2, seq_limit_def, archimedean — 這一步用到 I(f,0,3) 的存在（G2）。反向不宣稱：單看一族左端和收斂，不能推出函數可積；MKO 段落 0 也提醒，定義要求所有合法標記分割的共同極限。
- S02 · premise_audit · G3, riemann_limit_meaning, order_basics — 需要 N≥1，Δx=3/N 才有定義且為正。只宣稱每個左端和是標記分割和；反向（每個標記分割和都是左端和）並不成立，也不宣稱。
- S01 · premise_audit · G1, G2, mko_riemann_def, riemann_limit_meaning — 此步只展開定義並記下存在性前提，不推出任何數值。存在性來自 G2（MKO 假設 a1），不是由後面某一族特殊的和收斂推出的。





## 錯誤控制與反例

有限左端和不是積分MKO 指出的常見誤解之一是把有限左端和當成積分。由 S09，誤差 |L_N+3|=(27N−9)/(2N²) 對每個 N≥1 都大於 0，所以沒有任何有限 N 的左端和等於 −3（例如 L_3=−7、L_50=−3.2682）；只有 N→∞ 的極限才等於積分。

反向端點要換號∫₃⁰ 與 ∫₀³ 的被積函數相同、方向相反，值為 3 而不是 −3。不能以「同一段區間」為由忽略方向，也不能一律取絕對值（MKO 假設 a2）。

有號積分不是面積f 在 [0,2) 為負、在 (2,3] 為正，兩段 −16/3 與 7/3 抵消成 −3；兩段絕對值之和 23/3 才是「不計正負」的量。把積分一律當非負面積，會把 −3 錯寫成 23/3 或 3。

矩核對不是一般 FTCS12 套用的是本 MKO 明列的多項式矩公式；它與 S11 一致只是兩條路互相核對。MKO 明說不把一般微積分基本定理當作已完成的前置，本稿也不宣稱證明了它。


- L_50=−3.2682 就是 ∫₀³(x²−4)dx → reject — L_50 與 −3 相差 (27·50−9)/(2·50²)=1341/5000≠0；積分是 N→∞ 的極限。
- ∫₃⁰(x²−4)dx=∫₀³(x²−4)dx=−3，因為是同一段區間 → reject — 反向規則給 I(f,3,0)=−I(f,0,3)=3。
- 定積分恆非負，所以 ∫₀³(x²−4)dx 應等於 23/3 → reject — 積分有號，值為 −3；23/3 是兩段絕對值之和。
- 只要某一族等分左端和收斂，函數就可積，積分就是那個極限 → reject — Dirichlet 函數 D（有理數處為 1、其餘為 0）在 [0,1] 上：左端點 i/N 都是有理數，所以每個左端和都是 1；但改取無理數標記，網格再小的和也都是 0，沒有共同極限，D 不是 Riemann 可積（MKO 段落 0）。





## 結論與限制

在 f 可積（MKO 假設 a1）的前提下，由 Riemann 定義與左端和 L_N=−3−27/(2N)+9/(2N²) 的極限得 ∫₀³(x²−4)dx=−3；MKO 的矩公式獨立給出同一值。反向端點 ∫₃⁰(x²−4)dx=3。有限左端和 L_3=−7、L_50=−3.2682 都不等於積分；兩段 −16/3 與 7/3 互相抵消，所以積分不是非負面積。


- f 的可積性（G2）取自 MKO 假設 a1，本稿未由定義證明；S03 依賴它。
- 矩公式（mko_moment）是 MKO 明列的規則；本稿只對 f(x)=x²−4 由定義獨立核對其值，未證明一般矩公式。
- N4、N10 是 N=1 到 50 的有限核對，只支持這些點；一般 N 的結論依賴 S07、S09 的代數與 N3 的多項式恆等式。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 1358dfe43443e21f9926bd2ea2dd97a3b9034b0966a92b412d106d4ae7195ad4
- original source SHA-256: 1358dfe43443e21f9926bd2ea2dd97a3b9034b0966a92b412d106d4ae7195ad4
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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