Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The final-time face is not part of the parabolic boundary

Statement refuted

The claim refuted is that every supersolution ut−Δu≥0 on a bounded cylinder Q satisfies max⁡Q‾u≤max⁡∂pQu. The witness has its larger maximum at a spatially interior point of the final-time face, which is excluded from the parabolic boundary. Take Ω=(0,π) and u(x,t):=etsin⁡x. Then ut=etsin⁡x and Δu=−etsin⁡x, so ut−Δu=2etsin⁡x≥0 in Q: u is a supersolution. Its maximum over the closed cylinder is max⁡Q‾u=eT, attained at the interior point (π/2,T) of the final-time face, whereas max⁡∂pQu=max⁡(max⁡[0,π]sin⁡,0)=1<eT because the lateral data vanish and the initial data are sin⁡x≤1 with equality at x=π/2. So the final-time face is not part of the parabolic boundary, and for a supersolution the maximum over the cylinder is genuinely larger than the parabolic-boundary maximum: the maximum principle is sign-sensitive and does not extend in the reverse direction.

Facts & Assumptions

Given: T>0, the cylinder Q=(0,π)×(0,T] with Q‾=[0,π]×[0,T], and the function u(x,t)=etsin⁡x.

[F1]

The cylinder vocabulary: ∂pQ=(Ω‾×{0})∪(∂Ω×[0,T]), no point of the final-time face belongs to ∂pQ, and ut−Δu≥0 in Q is imposed for 0<t≤T, with ut interpreted as the left time derivative at t=T (Parabolic cylinder and parabolic boundary).

[F2]

sin⁡ and cos⁡ are C∞ with (sin⁡x)′=cos⁡x and (cos⁡x)′=−sin⁡x, sin⁡0=0, cos⁡0=1 (The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series); sin⁡(π/2)=1, sin⁡π=0, and sin⁡x>0 for 0<x<π (Quarter-turn values and shifts by pi/2 and pi, Pi is the first positive zero of sine), while sin⁡ has range [−1,1] (Signs, monotonicity intervals, and ranges of sine and cosine).

[F4]

The Laplacian on R1 is Δf=f′′ (The Laplacian of a C2 function and of a C2 vector field), and the weak maximum principle on a bounded cylinder: a subsolution v∈C2,1(Q‾) with vt−Δv≤0 in Q satisfies max⁡Q‾v=max⁡∂pQv (Weak parabolic maximum principle).

Counterexample

Given: T>0, the cylinder Q=(0,π)×(0,T], and u(x,t)=etsin⁡x.

1.1F2F3F4given

The function u is smooth on Q‾ (a product of the smooth functions et and sin⁡x, [F2] and [F3]), with ut=etsin⁡x and Δu=uxx=−etsin⁡x by [F2] and [F4]; hence ut−Δu=2etsin⁡x≥0 on Q, because et>0 by [F3] and sin⁡x>0 for 0<x<π by [F2].

1.2F1F2given

On the parabolic boundary, u(0,t)=u(π,t)=etsin⁡π=0 for every t∈[0,T], and u(x,0)=sin⁡x≤1 with u(π/2,0)=1; hence max⁡∂pQu=1.

1.3F2F3given

For every (x,t)∈Q‾ one has sin⁡x≤1 by [F2] and et≤eT: indeed eT−et=ec(T−t)>0 for some c∈(t,T) whenever t<T by [F3] and the mean value theorem, so u(x,t)≤eT; equality holds exactly at (x,t)=(π/2,T), where u=eTsin⁡(π/2)=eT. Thus max⁡Q‾u=eT, attained at the point (π/2,T) of the final-time face.

2.1step 1.2step 1.3F1F3given

The point (π/2,T) does not belong to ∂pQ, because π/2∈(0,π) and T>0 by [F1]; by step 1.3 it is a point of Q‾ at which u attains the value eT, while by step 1.2 the parabolic boundary carries the strictly smaller maximum 1. Since eT>1 (again by the mean value theorem applied to exp⁡ on [0,T], [F3]), a supersolution has its maximum over Q‾ strictly larger than the parabolic-boundary maximum, refuting the proposed supersolution maximum bound. The minimum principle for supersolutions, obtained by applying the weak maximum principle to −u, remains valid.

3.1step 1.1step 1.2F1F4given∎

The sign sensitivity is real and the weak maximum principle is not contradicted: v:=−u satisfies vt−Δv=−2etsin⁡x≤0 on Q, and by [F4] its maximum over Q‾ equals max⁡∂pQv=0, attained on the lateral faces, consistently with the theorem being stated for subsolutions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources