邊界值問題：矩形上 Poisson–Dirichlet 問題的內部與四邊分開核對

目標與範圍

在矩形 Ω=(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 的值。

逐步主鏈

\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

u=x^2+xy+y^2

u_x=2x+y,\ u_y=x+2y

u_x=2x+y,\ u_y=x+2y

u_{xx}=2,\ u_{yy}=2

\Delta u-4=u_{xx}+u_{yy}-4

\Delta u-4=2+2-4=0\ \text{(zero polynomial)};\ (I)\ \text{holds}

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

u|_{\Gamma_L}=u(0,y)

u(0,y)=y^2=g_L(y)\ \ (\text{coefficients } (1,0,0)=(1,0,0))

u|_{\Gamma_R}=u(2,y)

u(2,y)=y^2+2y+4=g_R(y)\ \ (\text{coefficients } (1,2,4)=(1,2,4))

u|_{\Gamma_B}=u(x,0)

u(x,0)=x^2=g_B(x)\ \ (\text{coefficients } (1,0,0)=(1,0,0))

u|_{\Gamma_T}=u(x,1)

u(x,1)=x^2+x+1=g_T(x)\ \ (\text{coefficients } (1,1,1)=(1,1,1))

u=g_L,\ u=g_R,\ u=g_B,\ u=g_T\ \text{on their edges}

(B)\ \text{holds for } u

(I)\ \text{for } u,\ (B)\ \text{for } u

u\ \text{satisfies the declared BVP}

v=2x^2+xy-2x+y

\Delta v-4=4+0-4=0;\ (I)\ \text{holds for } v

v(0,0),\ v(2,0),\ v(0,1),\ v(2,1)

0,\ 4,\ 1,\ 7\ =\ g\ \text{at the four corners}

v|_{\Gamma_B}=v(x,0)

v(x,0)=2x^2-2x\neq x^2;\ v(1,0)=0\neq 1=g_B(1)

v|_{\Gamma_L}=v(0,y)

v(0,y)=y\neq y^2;\ v(0,\tfrac12)=\tfrac12\neq\tfrac14=g_L(\tfrac12)

(I)\ \text{for } v,\ v(1,0)\neq g_B(1)

(B)\ \text{fails for } v;\ v\ \text{does not satisfy the declared BVP}

局部子步與引理

v=2x^2+xy-2x+y

v_x=4x+y-2,\ v_y=x+1

v_x=4x+y-2,\ v_y=x+1

v_{xx}=4,\ v_{yy}=0,\ \Delta v=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、反控制與修訂記錄）