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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-boundary-value-problem/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-boundary-value-problem-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

\text{declared BVP on } \Omega=(0,2)\times(0,1)

After

(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

Conditions: none

Rule: mko_bvp · Uses: G1, G2, mko_bvp

Leaf basis: mko_bvp + def_unfold

By the MKO, 'the candidate satisfies the declared BVP' consists of two distinct groups of obligations: (I) the interior Poisson equation Δu=4 holds at every point of Ω; (B) u equals the Dirichlet data at every point of the four edges. The two groups are written down separately first; each gets its own evidence, and only then are they combined.



S02 · impliesBefore

u=x^2+xy+y^2

After

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

Conditions: none

Rule: poly_partial · Uses: G3, poly_partial

Leaf basis: poly_partial

Differentiate term by term: ∂x(x²)=2x, ∂x(xy)=y, ∂x(y²)=0, giving u_x=2x+y; ∂y(x²)=0, ∂y(xy)=x, ∂y(y²)=2y, giving u_y=x+2y.



S03 · impliesBefore

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

After

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

Conditions: none

Rule: poly_partial · Uses: S02, poly_partial

Leaf basis: poly_partial

u_xx=∂x(2x+y)=2 and u_yy=∂y(x+2y)=2. The Laplacian needs only these two pure second partials.



S04 · impliesBefore

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

After

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

Conditions: none

Rule: poly_coeff_zero · Uses: S03, S01, poly_coeff_zero

Leaf basis: poly_coeff_zero + numeric_evaluation + forall_intro

Δu−4=2+2−4=0. The interior residual is the zero polynomial (the constant 0), so it equals 0 at every point of Ω, indeed of ℝ². This is a symbolic identity, not a check at a few interior points. Record: u satisfies obligation (I).



S05 · equivalentBefore

u=g\ \text{on}\ \partial\Omega

After

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

Conditions: none

Rule: set_operations_def · Uses: G1, S01, set_operations_def

Leaf basis: set_operations_def + and_intro_elim

∂Ω=Γ_L∪Γ_R∪Γ_B∪Γ_T (G1). A point lies in the union exactly when it lies on some edge, so 'u equals the data at every point of ∂Ω' is equivalent to 'u equals the data at every point of each of the four edges'. None of the four conjuncts may be dropped.



S06 · impliesBefore

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

After

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

Conditions: 0\le y\le 1

Rule: edge_restrict · Uses: S05, G2, G3, edge_restrict, poly_coeff_zero

Leaf basis: edge_restrict + poly_coeff_zero + numeric_evaluation

Left edge x=0: u(0,y)=0²+0·y+y²=y². In terms of the coefficients of (y², y, 1), the restriction is (1,0,0) and the data g_L are also (1,0,0); the coefficients agree, so u=g_L on the whole left edge (every y∈[0,1]). This is an identity on the whole edge, not a check at a few values of y.



S07 · impliesBefore

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

After

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

Conditions: 0\le y\le 1

Rule: edge_restrict · Uses: S05, G2, G3, edge_restrict, poly_coeff_zero

Leaf basis: edge_restrict + poly_coeff_zero + numeric_evaluation

Right edge x=2: u(2,y)=2²+2y+y²=y²+2y+4. The coefficients (1,2,4) equal those of g_R, (1,2,4), so u=g_R on the whole right edge.



S08 · impliesBefore

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

After

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

Conditions: 0\le x\le 2

Rule: edge_restrict · Uses: S05, G2, G3, edge_restrict, poly_coeff_zero

Leaf basis: edge_restrict + poly_coeff_zero + numeric_evaluation

Bottom edge y=0: u(x,0)=x²+x·0+0²=x². The coefficients of (x², x, 1), namely (1,0,0), equal those of g_B, so u=g_B on the whole bottom edge.



S09 · impliesBefore

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

After

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

Conditions: 0\le x\le 2

Rule: edge_restrict · Uses: S05, G2, G3, edge_restrict, poly_coeff_zero

Leaf basis: edge_restrict + poly_coeff_zero + numeric_evaluation

Top edge y=1: u(x,1)=x²+x·1+1²=x²+x+1. The coefficients (1,1,1) equal those of g_T, so u=g_T on the whole top edge.



S10 · impliesBefore

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

After

(B)\ \text{holds for } u

Conditions: none

Rule: and_intro_elim · Uses: S05, S06, S07, S08, S09

Leaf basis: and_intro_elim + set_operations_def

The identities on all four edges are proved (S06 to S09); by conjunction introduction and the equivalence of S05, u equals the Dirichlet data on all of ∂Ω. Record: u satisfies obligation (B).



S11 · impliesBefore

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

After

u\ \text{satisfies the declared BVP}

Conditions: none

Rule: and_intro_elim · Uses: S04, S10, S01

Leaf basis: and_intro_elim + mko_bvp

Both groups of obligations have been recorded separately (S04 and S10), so by the MKO one may now say that u satisfies the declared BVP. A side observation: the data at each corner come from two edges and agree, for example at (2,1) g_R(1)=1+2+4=7=g_T(2)=4+2+1, consistent with both being restrictions of one function.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: poly_partial · Uses: G3, poly_partial

Leaf basis: poly_partial + poly_coeff_zero

By S12.1 and S12.2, v_xx=4 and v_yy=0, so Δv−4=0 is the zero polynomial and v also satisfies the interior obligation (I). Note that v=u+h with h=x²−y²−2x+y harmonic (h_xx+h_yy=2−2=0), so the interior obligation cannot tell u and v apart.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G2, G3

Leaf basis: numeric_evaluation

The four corners: v(0,0)=0 with data g_B(0)=0; v(2,0)=8+0−4+0=4 with data g_B(2)=4; v(0,1)=0+0−0+1=1 with data g_L(1)=1; v(2,1)=8+2−4+1=7 with data g_R(1)=7. All four corners match, because h vanishes at all four corners. Checking only the corners would wrongly suggest that v meets the boundary data.



S14 · impliesBefore

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

After

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

Conditions: 0\le x\le 2

Rule: edge_restrict · Uses: S05, G2, G3, edge_restrict

Leaf basis: edge_restrict + numeric_evaluation

Bottom edge y=0: v(x,0)=2x²+0−2x+0=2x²−2x. The coefficients (2,−2,0) differ from those of g_B, (1,0,0). Take the point x=1∈[0,2] on the bottom edge: v(1,0)=2−2=0 while g_B(1)=1, so v does not equal the data on the bottom edge. Their difference v(x,0)−x²=x(x−2) vanishes only at x=0 and x=2, the two corners.



S15 · impliesBefore

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

After

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

Conditions: 0\le y\le 1

Rule: edge_restrict · Uses: S05, G2, G3, edge_restrict

Leaf basis: edge_restrict + numeric_evaluation

Left edge x=0: v(0,y)=0+0−0+y=y, with coefficients (0,1,0) differing from those of g_L, (1,0,0); at y=1/2∈[0,1], v=1/2 while g_L=1/4. The left edge fails as well. (On the right, v(2,y)=3y+4, and on the top, v(x,1)=2x²−x+1, also differ from the data; this guide does not expand them further.)



S16 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: S05, S12, S13, S14, quantifier_negation

Leaf basis: quantifier_negation + and_intro_elim + exists_intro

(B) is the universal statement 'equal at every boundary point'; S14 gives one boundary point where they differ, so by quantifier negation (B) fails for v. The BVP requires (I) and (B) together, so v does not satisfy the declared BVP, even though (I) holds (S12) and all four corners match (S13).







## Substeps and lemmas

S12.1 · impliesBefore

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

After

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

Conditions: none

Rule: poly_partial · Uses: G3, poly_partial

Leaf basis: poly_partial

∂x(2x²)=4x, ∂x(xy)=y, ∂x(−2x)=−2, ∂x(y)=0, giving v_x=4x+y−2; ∂y(2x²)=0, ∂y(xy)=x, ∂y(−2x)=0, ∂y(y)=1, giving v_y=x+1.



S12.2 · impliesBefore

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

After

v_{xx}=4,\ v_{yy}=0,\ \Delta v=4

Conditions: none

Rule: poly_partial · Uses: S12.1, poly_partial

Leaf basis: poly_partial + numeric_evaluation

v_xx=∂x(4x+y−2)=4 and v_yy=∂y(x+1)=0, so Δv=4+0=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 enoughThe 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 boundsv 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-posednessS11 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-boundary-value-problem-01.json)