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

目標與範圍

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

逐步主鏈

I(f,0,3)

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

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}

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

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

f(x_i)\,\Delta x

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

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

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

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

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}

L_3,\ L_{50}

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

|L_N-(-3)|

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

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

L_N\to -3

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

I(f,0,3)=-3

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

I(f,3,0)

-I(f,0,3)=3

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

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

|I(f,0,3)|

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

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

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

局部子步與引理

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

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

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

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

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

逐步反向審查

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

矩核對不是一般 FTC

S12 套用的是本 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、反控制與修訂記錄）