# 邊界值問題：矩形上 Poisson–Dirichlet 問題的內部與四邊分開核對 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-boundary-value-problem/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-boundary-value-problem-01 · production-20261019-adopted-96 ## 目標與範圍 在矩形 Ω=(0,2)×(0,1) 上宣告 BVP：內部 Δu=u_xx+u_yy=4；Dirichlet 資料為左邊 u(0,y)=y²、右邊 u(2,y)=y²+2y+4（0≤y≤1）、下邊 u(x,0)=x²、上邊 u(x,1)=x²+x+1（0≤x≤2）。對二次多項式候選 u=x²+xy+y² 與 v=2x²+xy−2x+y，分別記錄內部 Poisson 義務（符號 Laplacian 恆等式）與四條邊的 Dirichlet 義務（精確限制到整條邊後逐係數比較），判定誰滿足此宣告的 BVP，並說明 v 為何在內部方程成立、四個角點也都吻合的情況下仍不滿足。 停在 MKO 的切片內：矩形域、二次多項式候選、符號 Laplacian 恆等式、四條邊的精確限制與係數比較。符號約定明示為 Δu=u_xx+u_yy，方程寫成 Δu=4。核對成功的候選給出此特定 BVP 的存在見證，但不證一般存在定理或唯一、穩定、正則與適定性；不處理弱解或函數空間；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - numeric_evaluation - distributive - eq_replace - poly_partial - set_operations_def - quantifier_negation - G1 — Ω=(0,2)×(0,1)，其閉包為 [0,2]×[0,1]；邊界恰由四條閉邊組成：Γ_L={0}×[0,1]、Γ_R={2}×[0,1]、Γ_B=[0,2]×{0}、Γ_T=[0,2]×{1}。 - G2 — 宣告的 BVP：在 Ω 內 Δu=u_xx+u_yy=4；Dirichlet 資料 g_L(y)=y²、g_R(y)=y²+2y+4（y∈[0,1]），g_B(x)=x²、g_T(x)=x²+x+1（x∈[0,2]），要求 u 在每條邊上等於對應資料。 - G3 — 兩個二次多項式候選：u=x²+xy+y²，v=2x²+xy−2x+y。 - \Omega=(0,2)\times(0,1) — 開矩形（內部） - \Gamma_L,\Gamma_R,\Gamma_B,\Gamma_T — 左、右、下、上四條閉邊 - \Delta u=u_{xx}+u_{yy} — Laplacian - u|_{\Gamma} — u 限制到邊 Γ 上所得的單變數多項式 - (I),\ (B) — 內部義務與邊界義務 - h=x^2-y^2-2x+y — 調和多項式，v=u+h ## 規則與來源 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - mko_bvp · cited — 本輪固定矩形域上的二次多項式候選 u。內部 Poisson 責任以符號 Laplacian 恆等核對，Dirichlet 資料則把 u 精確限制到四條邊並逐係數比較；兩類責任分開記錄後，才可說候選滿足該宣告 BVP。符號恆等只核指定候選與指定方程／邊界，不證一般解存在、唯一、穩定、正則或適定。 · mko-boundary-value-problem - poly_partial · prerequisite — 多項式的偏導數：∂/∂x 逐項且線性地作用，把 y 視為常數，∂/∂x(x^m y^k)=m x^(m−1) y^k（m≥1），m=0 時為 0；∂/∂y 對稱地作用。 - poly_coeff_zero · prerequisite — 係數全為 0 的多項式（一變數或二變數）在每一點取值都是 0；因此兩個係數逐一相同的多項式在每一點取值相同。 - edge_restrict · prerequisite — 把二變數多項式限制到一條邊，就是把該邊固定的座標（x=0、x=2、y=0 或 y=1）代入；結果是剩下變數的多項式，在該邊的每一點都給出 u 的值。 ## 逐步主鏈 S01 · definition操作前 \text{declared BVP on } \Omega=(0,2)\times(0,1) 操作後 (I):\ \Delta u-4\equiv 0\ \text{in}\ \Omega;\quad (B):\ u|_{\Gamma_L}=y^2,\ u|_{\Gamma_R}=y^2+2y+4,\ u|_{\Gamma_B}=x^2,\ u|_{\Gamma_T}=x^2+x+1 條件：無 規則：mko_bvp · 依賴：G1, G2, mko_bvp 葉節點依據：mko_bvp + def_unfold 依 MKO，「候選滿足宣告的 BVP」由兩組不同的義務組成：(I) 內部 Poisson 方程 Δu=4 在 Ω 的每一點成立；(B) u 在四條邊的每一點等於 Dirichlet 資料。先把兩組義務分開寫下，之後各自取得證據，最後才合併。 S02 · implies操作前 u=x^2+xy+y^2 操作後 u_x=2x+y,\ u_y=x+2y 條件：無 規則：poly_partial · 依賴：G3, poly_partial 葉節點依據：poly_partial 逐項求偏導：∂x(x²)=2x、∂x(xy)=y、∂x(y²)=0，得 u_x=2x+y；∂y(x²)=0、∂y(xy)=x、∂y(y²)=2y，得 u_y=x+2y。 S03 · implies操作前 u_x=2x+y,\ u_y=x+2y 操作後 u_{xx}=2,\ u_{yy}=2 條件：無 規則：poly_partial · 依賴：S02, poly_partial 葉節點依據：poly_partial u_xx=∂x(2x+y)=2，u_yy=∂y(x+2y)=2。Laplacian 只需要這兩個純二階偏導。 S04 · implies操作前 \Delta u-4=u_{xx}+u_{yy}-4 操作後 \Delta u-4=2+2-4=0\ \text{(zero polynomial)};\ (I)\ \text{holds} 條件：無 規則：poly_coeff_zero · 依賴：S03, S01, poly_coeff_zero 葉節點依據：poly_coeff_zero + numeric_evaluation + forall_intro Δu−4=2+2−4=0。內部殘差是零多項式（常數 0），所以在 Ω 的每一點、事實上在 ℝ² 的每一點都等於 0。這是符號恆等，不是在內部取幾個點核對。記錄：u 滿足義務 (I)。 S05 · equivalent操作前 u=g\ \text{on}\ \partial\Omega 操作後 u=g_L\ \text{on}\ \Gamma_L\ \land\ u=g_R\ \text{on}\ \Gamma_R\ \land\ u=g_B\ \text{on}\ \Gamma_B\ \land\ u=g_T\ \text{on}\ \Gamma_T 條件：無 規則：set_operations_def · 依賴：G1, S01, set_operations_def 葉節點依據：set_operations_def + and_intro_elim ∂Ω=Γ_L∪Γ_R∪Γ_B∪Γ_T（G1）。一個點在聯集中，當且僅當它在某一條邊上；所以「在 ∂Ω 的每一點 u 等於資料」等價於「在四條邊的每一條的每一點都相等」。四個合取項缺一不可。 S06 · implies操作前 u|_{\Gamma_L}=u(0,y) 操作後 u(0,y)=y^2=g_L(y)\ \ (\text{coefficients } (1,0,0)=(1,0,0)) 條件：0\le y\le 1 規則：edge_restrict · 依賴：S05, G2, G3, edge_restrict, poly_coeff_zero 葉節點依據：edge_restrict + poly_coeff_zero + numeric_evaluation 左邊 x=0：u(0,y)=0²+0·y+y²=y²。按 (y², y, 1) 的係數，限制結果為 (1,0,0)，資料 g_L 也是 (1,0,0)，逐係數相同，所以在整條左邊（每個 y∈[0,1]）u=g_L。這是全邊恆等，不是抽查幾個 y。 S07 · implies操作前 u|_{\Gamma_R}=u(2,y) 操作後 u(2,y)=y^2+2y+4=g_R(y)\ \ (\text{coefficients } (1,2,4)=(1,2,4)) 條件：0\le y\le 1 規則：edge_restrict · 依賴：S05, G2, G3, edge_restrict, poly_coeff_zero 葉節點依據：edge_restrict + poly_coeff_zero + numeric_evaluation 右邊 x=2：u(2,y)=2²+2y+y²=y²+2y+4。係數 (1,2,4) 與 g_R 的 (1,2,4) 相同，所以在整條右邊 u=g_R。 S08 · implies操作前 u|_{\Gamma_B}=u(x,0) 操作後 u(x,0)=x^2=g_B(x)\ \ (\text{coefficients } (1,0,0)=(1,0,0)) 條件：0\le x\le 2 規則：edge_restrict · 依賴：S05, G2, G3, edge_restrict, poly_coeff_zero 葉節點依據：edge_restrict + poly_coeff_zero + numeric_evaluation 下邊 y=0：u(x,0)=x²+x·0+0²=x²。按 (x², x, 1) 的係數 (1,0,0) 與 g_B 相同，所以在整條下邊 u=g_B。 S09 · implies操作前 u|_{\Gamma_T}=u(x,1) 操作後 u(x,1)=x^2+x+1=g_T(x)\ \ (\text{coefficients } (1,1,1)=(1,1,1)) 條件：0\le x\le 2 規則：edge_restrict · 依賴：S05, G2, G3, edge_restrict, poly_coeff_zero 葉節點依據：edge_restrict + poly_coeff_zero + numeric_evaluation 上邊 y=1：u(x,1)=x²+x·1+1²=x²+x+1。係數 (1,1,1) 與 g_T 相同，所以在整條上邊 u=g_T。 S10 · implies操作前 u=g_L,\ u=g_R,\ u=g_B,\ u=g_T\ \text{on their edges} 操作後 (B)\ \text{holds for } u 條件：無 規則：and_intro_elim · 依賴：S05, S06, S07, S08, S09 葉節點依據：and_intro_elim + set_operations_def 四條邊的恆等都已證明（S06 至 S09）；依合取引入與 S05 的等價，u 在整個 ∂Ω 上等於 Dirichlet 資料。記錄：u 滿足義務 (B)。 S11 · implies操作前 (I)\ \text{for } u,\ (B)\ \text{for } u 操作後 u\ \text{satisfies the declared BVP} 條件：無 規則：and_intro_elim · 依賴：S04, S10, S01 葉節點依據：and_intro_elim + mko_bvp 兩組義務都已分開記錄（S04 與 S10），依 MKO 此時才可說 u 滿足宣告的 BVP。附帶觀察：每個角點的資料來自兩條邊，而且一致，例如 (2,1) 處 g_R(1)=1+2+4=7=g_T(2)=4+2+1，與它們都是同一個函數的限制相符。 S12 · implies操作前 v=2x^2+xy-2x+y 操作後 \Delta v-4=4+0-4=0;\ (I)\ \text{holds for } v 條件：無 規則：poly_partial · 依賴：G3, poly_partial 葉節點依據：poly_partial + poly_coeff_zero 依 S12.1、S12.2，v_xx=4、v_yy=0，所以 Δv−4=0 是零多項式，v 也滿足內部義務 (I)。注意 v=u+h，其中 h=x²−y²−2x+y 是調和的（h_xx+h_yy=2−2=0），所以內部義務不能區分 u 與 v。 S13 · implies操作前 v(0,0),\ v(2,0),\ v(0,1),\ v(2,1) 操作後 0,\ 4,\ 1,\ 7\ =\ g\ \text{at the four corners} 條件：無 規則：numeric_evaluation · 依賴：G2, G3 葉節點依據：numeric_evaluation 四個角點：v(0,0)=0，資料 g_B(0)=0；v(2,0)=8+0−4+0=4，資料 g_B(2)=4；v(0,1)=0+0−0+1=1，資料 g_L(1)=1；v(2,1)=8+2−4+1=7，資料 g_R(1)=7。四個角點全部吻合，因為 h 在四個角點都為 0。只抽查角點會誤以為 v 符合邊界資料。 S14 · implies操作前 v|_{\Gamma_B}=v(x,0) 操作後 v(x,0)=2x^2-2x\neq x^2;\ v(1,0)=0\neq 1=g_B(1) 條件：0\le x\le 2 規則：edge_restrict · 依賴：S05, G2, G3, edge_restrict 葉節點依據：edge_restrict + numeric_evaluation 下邊 y=0：v(x,0)=2x²+0−2x+0=2x²−2x。係數 (2,−2,0) 與 g_B 的 (1,0,0) 不同。取下邊上的點 x=1∈[0,2]：v(1,0)=2−2=0，而 g_B(1)=1，所以 v 在下邊不等於資料。兩者之差 v(x,0)−x²=x(x−2) 只在 x=0 與 x=2（兩個角點）為零。 S15 · implies操作前 v|_{\Gamma_L}=v(0,y) 操作後 v(0,y)=y\neq y^2;\ v(0,\tfrac12)=\tfrac12\neq\tfrac14=g_L(\tfrac12) 條件：0\le y\le 1 規則：edge_restrict · 依賴：S05, G2, G3, edge_restrict 葉節點依據：edge_restrict + numeric_evaluation 左邊 x=0：v(0,y)=0+0−0+y=y，係數 (0,1,0) 與 g_L 的 (1,0,0) 不同；在 y=1/2∈[0,1]，v=1/2 而 g_L=1/4。左邊同樣失敗。（右邊 v(2,y)=3y+4 與上邊 v(x,1)=2x²−x+1 也與資料不同，本稿不再逐一展開。） S16 · implies操作前 (I)\ \text{for } v,\ v(1,0)\neq g_B(1) 操作後 (B)\ \text{fails for } v;\ v\ \text{does not satisfy the declared BVP} 條件：無 規則：quantifier_negation · 依賴：S05, S12, S13, S14, quantifier_negation 葉節點依據：quantifier_negation + and_intro_elim + exists_intro (B) 是「邊界上每一點都相等」的全稱命題；S14 給出一個不相等的邊界點，依量詞否定 (B) 對 v 不成立。BVP 要求 (I) 與 (B) 同時成立，所以 v 不滿足宣告的 BVP，儘管 (I) 成立（S12）而且四個角點都吻合（S13）。 ## 局部子步與引理 S12.1 · implies操作前 v=2x^2+xy-2x+y 操作後 v_x=4x+y-2,\ v_y=x+1 條件：無 規則：poly_partial · 依賴：G3, poly_partial 葉節點依據：poly_partial ∂x(2x²)=4x、∂x(xy)=y、∂x(−2x)=−2、∂x(y)=0，得 v_x=4x+y−2；∂y(2x²)=0、∂y(xy)=x、∂y(−2x)=0、∂y(y)=1，得 v_y=x+1。 S12.2 · implies操作前 v_x=4x+y-2,\ v_y=x+1 操作後 v_{xx}=4,\ v_{yy}=0,\ \Delta v=4 條件：無 規則：poly_partial · 依賴：S12.1, poly_partial 葉節點依據：poly_partial + numeric_evaluation v_xx=∂x(4x+y−2)=4，v_yy=∂y(x+1)=0，所以 Δv=4+0=4。 ## 逐步反向審查 - S16 · premise_audit · S05, S14, quantifier_negation, and_intro_elim — 需要一個精確的反例點與「兩組義務都必須成立」。不宣稱 v 在邊界的每一點都不等於資料（角點就相等）。 - S15 · premise_audit · edge_restrict, G2, numeric_evaluation — 一個邊上的點就足以否證該邊義務。括號中的另外兩條邊只是補充，S16 不依賴它們。 - S14 · premise_audit · edge_restrict, G2, numeric_evaluation — 否證只需邊上一個精確的點；x=1 確實在 [0,2] 內。係數不同提示失敗，具體的點證實它。 - S13 · premise_audit · G2, G3, numeric_evaluation — 只是四個點的精確求值；不推出 v 在任何整條邊上等於資料。 - S12.2 · premise_audit · S12.1, poly_partial — 需要 S12.1 的一階偏導。 - S12.1 · premise_audit · poly_partial — 只用多項式求導規則。 - S12 · premise_audit · G3, poly_partial, poly_coeff_zero — 需要 v 的兩個純二階偏導（在子步 S12.1、S12.2 中算出）與零多項式處處為零。本步只處理 v 的 (I)。 - S11 · premise_audit · S04, S10, mko_bvp — 只是合取兩組已證的義務。不宣稱這個 BVP 的解唯一、穩定或適定（MKO a2）。 - S10 · premise_audit · S05, S06, S07, S08, S09, and_intro_elim — 需要四條邊全部；少核任一條且沒有其他涵蓋它的證明時，(B) 就尚未建立；不是據此斷言邊界條件為假。 - S09 · premise_audit · edge_restrict, poly_coeff_zero, G2 — 代入 y=1 後逐係數比較；只宣稱上邊義務。 - S08 · premise_audit · edge_restrict, poly_coeff_zero, G2 — 代入 y=0 後逐係數比較；只宣稱下邊義務。 - S07 · premise_audit · edge_restrict, poly_coeff_zero, G2 — 同 S06，代入 x=2 後逐係數比較；只宣稱右邊義務。 - S06 · premise_audit · edge_restrict, poly_coeff_zero, G2 — 需要精確代入 x=0 與係數相同推出處處相等。只宣稱左邊這一條義務。 - S05 · inverse_equivalence · set_operations_def, G1 — 聯集的定義是雙向的；四條邊的條件合起來恰好是整個邊界的條件。 - S04 · premise_audit · S03, poly_coeff_zero — 需要兩個二階偏導與零多項式處處為零。本步只處理 (I)，對邊界沒有任何結論。 - S03 · premise_audit · S02, poly_partial — 需要 S02 的一階偏導；不宣稱反向。 - S02 · premise_audit · G3, poly_partial — 只用多項式求導規則；不宣稱可由偏導唯一回推 u。 - S01 · premise_audit · G1, G2, mko_bvp — 此步只整理宣告，不推出新事實。四條邊必須完整列出（MKO a1），否則 (B) 會漏掉一部分邊界。 ## 錯誤控制與反例 只核內部方程不夠MKO 指出的誤解是只核內部 PDE 就宣稱 BVP 已解。v 的 Δv=4 恆成立，與 u 一樣通過 (I)，但違反邊界資料。內部義務與邊界義務必須分開記錄、分別證明。 角點不足；全邊可用係數或次數界證書v 在四個角點都吻合（S13），但下邊差 v(x,0)−x²=x(x−2) 只在兩個角點為零。此稿採整條邊的多項式係數比較作證書；沒有額外前提的幾個點不能取代全邊證明。但若已證差多項式次數至多 2，三個相異點為零就可由多項式根數界推出恆零；這是另一種帶次數界的完整證書，不是角點抽樣本身足夠。 滿足宣告的 BVP 不是適定性S11 只說 u 是這一組資料下的一個候選解。是否唯一、對資料擾動是否穩定，需要另外的定理（例如最大值原理類結果），本稿沒有證明也沒有引用。 - v 滿足 Δv=4，所以 v 解出這個 BVP → reject — 邊界義務失敗：v(1,0)=0≠1=g_B(1)。 - v 在四個角點都等於邊界資料，所以 v 滿足 Dirichlet 條件 → reject — 下邊在 x=1 不符（0 對 1），左邊在 y=1/2 不符（1/2 對 1/4）。 - w=(x+y)² 滿足 Δw=4 且在左邊、下邊都等於資料，所以 w 滿足此 BVP → reject — 四條邊都要核：右邊 w(2,1)=9≠7=g_R(1)。 - u 滿足此 BVP，所以這個 BVP 的解唯一且對資料穩定 → reject — 符號恆等只核指定候選；唯一性與穩定性需要另外的定理，MKO a2 明確排除這類推論。 ## 結論與限制 u=x²+xy+y² 滿足宣告的 BVP：內部 Δu−4 是零多項式（義務 (I)），且限制到四條邊後逐係數等於 y²、y²+2y+4、x²、x²+x+1（義務 (B)）。v=2x²+xy−2x+y 雖然 Δv=4 且在四個角點都吻合，但 v(x,0)=2x²−2x 在 x=1 處為 0≠1，所以不滿足此 BVP。已核對的 u 是此特定 BVP 的解存在見證；本結果不給一般存在定理，也不證唯一性或適定性。 - 本稿不證明也不引用 Dirichlet–Poisson 問題的唯一性或穩定性結果；這些屬於 MKO 的 formal next。 - S15 括號中右邊與上邊的失敗只是補充說明，N 系列只核了下邊與左邊的見證點。 ## 驗證及來源綁定 17 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: bbbc47a9eaa572e972cb4678073ca74403dc1f89cbba8026999be6bdd3be0414 - original source SHA-256: 95cd648e4ae4e97fe1b121a19464dc1e55260bc5fc03d901cdf37eea033e9390 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-boundary-value-problem-01.json)