Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass
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.

No-flux rectangular TPFA Lie error by even reflection

Statement

Let Ω=∏j=1d(0,Lj) and let u∈C1([0,T];C4(Ω‾;Rm)) solve ut=DΔu+F(u) with D=diag⁡(dr), dr≥0, and range in a compact reaction-inward rectangle R. Assume F∈C2 near R, homogeneous Neumann data hold, and the coordinatewise even reflection of u across every face extends to a Ct1Cx4 function on the doubled torus ∏j(R/2LjZ). On the uniform cell-centered grid of Cell-centered rectangular TPFA grid with homogeneous no-flux boundaries, start the exact reaction-then-diffusion Lie step of Exact reaction-then-diffusion Lie step on FV or periodic grids from cell-center samples and use uniform τ=T/N. Then a constant CT, independent of the mesh widths and N, satisfies

max⁡0≤n≤N∥Un−Phu(tn)∥∞≤CT(τ+hmax⁡2),tn=nτ.

This result is for rectangular Cartesian TPFA grids and solutions with the stated even C4 boundary compatibility; it does not assert mesh-uniform accuracy for general admissible polyhedral meshes.

Facts & Assumptions

Given: The rectangular no-flux TPFA grid, the periodic centered grid on the doubled torus, a smooth even-reflectable solution in R, and exact reaction-then-diffusion subflows.

[F1]

Cell-centered rectangular TPFA grid with homogeneous no-flux boundaries: the no-flux stencil uses the actual adjacent neighbor in the interior and a reflected copy of the boundary cell for a missing neighbor; Eh copies each cell value evenly to the doubled grid.

[F2]

Periodic rectangular reaction-diffusion grid: on the doubled grid the positive stencil is the periodic centered operator with widths hj.

[F3]

Mesh-uniform first-order Lie error for a smooth periodic reaction-diffusion solution: for a smooth periodic solution in R, the exact periodic Lie iterates from sampled data have maximum-norm error at most CT(τ+hmax⁡2) with a mesh-independent constant.

[F4]

Exact reaction-then-diffusion Lie step on FV or periodic grids: the step is the pointwise exact reaction flow followed by the exact specieswise exponential diffusion map.

[F5]

Inward reaction fields preserve rectangles and stoichiometric mass: the reaction IVP is unique and its flow is defined for all finite nonnegative times on R.

[F6]

Finite matrix exponential series and its identities: finite matrix exponentials are defined by a convergent power series.

[A1]

The even reflection in the Statement is Ct1Cx4; in particular its derivatives through the boundary interfaces match, and it is periodic on the doubled torus.

Proof

1.1F1F2givenalgebra

For each coordinate define rj(kj)=kj if 0≤kj<Nj and rj(kj)=2Nj−1−kj if Nj≤kj<2Nj. Then (EhU)k=U(rj(kj))j. At an interior original index, the doubled periodic stencil uses the same two neighbors as AhN. At the left boundary, the doubled neighbor kj=−1 is represented by 2Nj−1, whose reflected index is 0, so its value is Ui; the right-boundary ghost similarly equals the last cell value. Therefore A2hperEhU=EhAhNU for every array U.

2.1F4F5F6step 1.1inductionalgebra

From step 1.1, (A2hper)kEh=Eh(AhN)k for every integer k≥0, by induction. The exponential power series [F6] then gives e−τdrA2hperEh=Ehe−τdrAhN for each species. The nodewise reaction flow also commutes with Eh: reflected copies start from identical values and solve the same IVP, so uniqueness [F5] keeps them identical.

3.1F1F2F4step 2.1induction

At time zero, EhPhu(0) is exactly the sample of the even-reflected continuous initial data on the doubled torus. Step 2.1 shows that the periodic split update of this array is the even extension of the no-flux TPFA split update. Induction over n therefore identifies the periodic numerical iterates with EhUn.

4.1A1F1F2F3step 3.1algebra∎

The even-reflected function is Ct1Cx4 by [A1]. On every reflected open subrectangle, reflection preserves the Laplacian and acts only by coordinate sign changes on first derivatives; since the PDE has constant diagonal diffusion and pointwise reaction, the reflected function satisfies the same equation there. The equality extends across each interface by continuity of the function and its time and second spatial derivatives. Thus the doubled function solves the periodic problem covered by [F3]. Its samples are EhPhu(tn), and step 3.1 plus reflection gives ∥EhUn−EhPhu(tn)∥∞=∥Un−Phu(tn)∥∞. Apply [F3] on the doubled grid, whose counts 2Nj are at least four, to obtain the bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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