Boundary-value problem: checking the interior and all four edges separately for a Poisson–Dirichlet problem on a rectangle

Goal and scope

On the rectangle Ω=(0,2)×(0,1) declare the BVP: in the interior Δu=u_xx+u_yy=4; Dirichlet data u(0,y)=y² on the left, u(2,y)=y²+2y+4 on the right (0≤y≤1), u(x,0)=x² on the bottom and u(x,1)=x²+x+1 on the top (0≤x≤2). For the quadratic polynomial candidates u=x²+xy+y² and v=2x²+xy−2x+y, record separately the interior Poisson obligation (a symbolic Laplacian identity) and the Dirichlet obligation on all four edges (exact restriction to each whole edge, then coefficient comparison); decide which candidate satisfies this declared BVP, and explain why v fails although its interior equation holds and it matches the data at all four corners.

Stays inside the MKO's slice: a rectangular domain, quadratic polynomial candidates, a symbolic Laplacian identity, exact restriction to the four edges and coefficient comparison. The sign convention is explicit: Δu=u_xx+u_yy, and the equation is Δu=4. A successfully checked candidate witnesses existence for this particular BVP, but no general existence theorem, uniqueness, stability, regularity or well-posedness result is proved; weak solutions and function spaces are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• numeric_evaluation
• distributive
• eq_replace
• poly_partial
• set_operations_def
• quantifier_negation

• G1 — Ω=(0,2)×(0,1), with closure [0,2]×[0,1]; the boundary consists exactly of four closed edges: Γ_L={0}×[0,1], Γ_R={2}×[0,1], Γ_B=[0,2]×{0}, Γ_T=[0,2]×{1}.
• G2 — The declared BVP: Δu=u_xx+u_yy=4 in Ω; Dirichlet data g_L(y)=y² and g_R(y)=y²+2y+4 (y∈[0,1]), g_B(x)=x² and g_T(x)=x²+x+1 (x∈[0,2]), requiring u to equal the corresponding data on each edge.
• G3 — Two quadratic polynomial candidates: u=x²+xy+y² and v=2x²+xy−2x+y.

• \Omega=(0,2)\times(0,1) — the open rectangle (interior)
• \Gamma_L,\Gamma_R,\Gamma_B,\Gamma_T — the closed left, right, bottom and top edges
• \Delta u=u_{xx}+u_{yy} — the Laplacian
• u|_{\Gamma} — the one-variable polynomial obtained by restricting u to the edge Γ
• (I),\ (B) — the interior obligation and the boundary obligation
• h=x^2-y^2-2x+y — a harmonic polynomial, with v=u+h

Rules and sources

• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• mko_bvp · cited — This slice fixes a quadratic polynomial candidate u on a rectangle. A symbolic Laplacian identity checks the interior Poisson obligation; Dirichlet data are checked by restricting u exactly to all four edges and comparing polynomial coefficients. Only after separately recording both groups may the candidate be said to satisfy the declared BVP. Symbolic identities check only the specified candidate, equation and boundary data; they prove no general existence, uniqueness, stability, regularity or well-posedness theorem. · mko-boundary-value-problem
• poly_partial · prerequisite — Partial derivatives of polynomials: ∂/∂x acts termwise and linearly, treating y as a constant, with ∂/∂x(x^m y^k)=m x^(m−1) y^k for m≥1 and 0 for m=0; ∂/∂y acts symmetrically.
• poly_coeff_zero · prerequisite — A polynomial (in one or two variables) whose coefficients are all 0 takes the value 0 at every point; hence two polynomials with identical coefficients take equal values at every point.
• edge_restrict · prerequisite — Restricting a bivariate polynomial to an edge means substituting the coordinate fixed on that edge (x=0, x=2, y=0 or y=1); the result is a polynomial in the remaining variable that gives the value of u at every point of the edge.

Main derivation

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

Substeps and lemmas

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

Reverse audits

• S16 · premise_audit · S05, S14, quantifier_negation, and_intro_elim — It needs one exact counterexample point and the requirement that both groups hold. It does not claim that v differs from the data at every boundary point (it agrees at the corners).
• S15 · premise_audit · edge_restrict, G2, numeric_evaluation — One point on the edge suffices to refute that edge's obligation. The two further edges in parentheses are a remark only; S16 does not depend on them.
• S14 · premise_audit · edge_restrict, G2, numeric_evaluation — A refutation needs only one exact point on the edge; x=1 does lie in [0,2]. The differing coefficients signal the failure and the specific point confirms it.
• S13 · premise_audit · G2, G3, numeric_evaluation — This is exact evaluation at four points only; it does not imply that v equals the data on any whole edge.
• S12.2 · premise_audit · S12.1, poly_partial — It needs the first partials of S12.1.
• S12.1 · premise_audit · poly_partial — Only the differentiation rule for polynomials is used.
• S12 · premise_audit · G3, poly_partial, poly_coeff_zero — It needs the two pure second partials of v (computed in sub-steps S12.1 and S12.2) and that the zero polynomial vanishes everywhere. This step settles only (I) for v.
• S11 · premise_audit · S04, S10, mko_bvp — This only conjoins the two proved obligations. It does not claim that the BVP has a unique, stable or well-posed solution (MKO assumption a2).
• S10 · premise_audit · S05, S06, S07, S08, S09, and_intro_elim — All four edges are needed; if an edge is unverified and no other proof covers it, (B) is not established; this does not assert that the boundary condition is false.
• S09 · premise_audit · edge_restrict, poly_coeff_zero, G2 — Substitute y=1 and compare coefficients; only the top-edge obligation is claimed.
• S08 · premise_audit · edge_restrict, poly_coeff_zero, G2 — Substitute y=0 and compare coefficients; only the bottom-edge obligation is claimed.
• S07 · premise_audit · edge_restrict, poly_coeff_zero, G2 — As in S06: substitute x=2 and compare coefficients; only the right-edge obligation is claimed.
• S06 · premise_audit · edge_restrict, poly_coeff_zero, G2 — It needs the exact substitution x=0 and that equal coefficients give equality everywhere. Only the left-edge obligation is claimed.
• S05 · inverse_equivalence · set_operations_def, G1 — The definition of union is two-way; the four edge conditions together are exactly the condition on the whole boundary.
• S04 · premise_audit · S03, poly_coeff_zero — It needs the two second partials and that the zero polynomial vanishes everywhere. This step settles only (I) and says nothing about the boundary.
• S03 · premise_audit · S02, poly_partial — It needs the first partials of S02; no converse is claimed.
• S02 · premise_audit · G3, poly_partial — Only the differentiation rule for polynomials is used; it is not claimed that u can be recovered uniquely from its partials.
• S01 · premise_audit · G1, G2, mko_bvp — This step only organizes the declaration and derives no new fact. All four edges must be listed (MKO assumption a1); otherwise (B) would miss part of the boundary.

Error controls and negative controls

Checking only the interior equation is not enough

The mistake named by the MKO is to declare the BVP solved after checking only the interior PDE. v has Δv=4 identically and passes (I) just as u does, yet it violates the boundary data. The interior and boundary obligations must be recorded separately and proved separately.

Corners are insufficient; whole-edge certificates need coefficients or degree bounds

v matches all four corners (S13), but its bottom-edge difference v(x,0)−x²=x(x−2) vanishes only at the two corners. This guide uses whole-edge polynomial coefficient comparison as its certificate. A few points without additional premises do not replace a whole-edge proof. If the difference is proved to have degree at most 2, however, three distinct zeros force it to vanish identically by the polynomial root bound. That is a different complete certificate with a degree bound, not a claim that corners alone suffice.

Satisfying the declared BVP is not well-posedness

S11 says only that u is a candidate solution for this data. Whether it is unique, and whether it is stable under perturbations of the data, needs further theorems (for example results of maximum-principle type), which this guide neither proves nor cites.

• v satisfies Δv=4, so v solves this BVP → reject — The boundary obligation fails: v(1,0)=0≠1=g_B(1).
• v equals the boundary data at all four corners, so v satisfies the Dirichlet condition → reject — The bottom edge fails at x=1 (0 vs 1) and the left edge at y=1/2 (1/2 vs 1/4).
• w=(x+y)² satisfies Δw=4 and equals the data on the left and bottom edges, so w satisfies this BVP → reject — All four edges must be checked: on the right w(2,1)=9≠7=g_R(1).
• u satisfies this BVP, so the BVP has a unique solution that is stable under changes of the data → reject — Symbolic identities check only the specified candidate; uniqueness and stability need further theorems, and MKO assumption a2 explicitly excludes such inferences.

Result and limitations

u=x²+xy+y² satisfies the declared BVP: in the interior Δu−4 is the zero polynomial (obligation (I)), and its restrictions to the four edges equal y², y²+2y+4, x² and x²+x+1 coefficient by coefficient (obligation (B)). v=2x²+xy−2x+y has Δv=4 and matches the data at all four corners, but v(x,0)=2x²−2x equals 0≠1 at x=1, so v does not satisfy this BVP. The checked u witnesses existence for this particular BVP. No general existence theorem, uniqueness or well-posedness result is proved.

• This guide neither proves nor cites uniqueness or stability results for the Dirichlet–Poisson problem; these belong to the MKO's formal next.
• The failures on the right and top edges mentioned in parentheses in S15 are a remark only; the numeric checks cover only the witness points on the bottom and left edges.

Verification and source binding

17 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: bbbc47a9eaa572e972cb4678073ca74403dc1f89cbba8026999be6bdd3be0414
• original source SHA-256: 95cd648e4ae4e97fe1b121a19464dc1e55260bc5fc03d901cdf37eea033e9390
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)