ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

The tau term recovers the restricted root in reaction Poisson

Statement

For the finite-difference semilinear reaction operator $F_{h} (u) = A u + (u_{1}^{3}, u_{2}^{3})$ with $A = (\begin{array}{cc} 2 & - 1 \\ - 1 & 2 \end{array})$ , take $P = (1, 1)^{T}$ , $I u = (u_{1} + u_{2}) / 2$ , $R = P^{T}$ , and the Galerkin coarse operator $F_{H} (v) = P^{T} F_{h} (P v) = 2 v + 2 v^{3}$ . For the manufactured fine root $u_{*} = (1, 0)$ and $f_{h} = F_{h} (u_{*})$ , the tau correction is $- 3 / 4$ and the exact coarse branch returns $I u_{*} = 1 / 2$ , so the corrected fine iterate is still $u_{*}$ .

Facts & Assumptions

Given: The two residual maps, the transfers, $u_{*} = (1, 0)$ , and $f_{h} = F_{h} (u_{*})$ .

[F1]

Finite-budget nonlinear FAS two-grid cycle: the coarse target is $F_{H} (I u) + R (f_{h} - F_{h} (u)) = R f_{h} + τ (u)$ , where $τ (u) = F_{H} (I u) - R F_{h} (u)$ , and the fine correction is $u + P (v - I u)$ .

[F2]

An exact fine root is fixed by the FAS V/W cycle: if the smoother fixes the fine root and the exact coarse solver selects its restriction at zero defect, FAS leaves the root fixed.

Example

Given: Exact real arithmetic and the direct coarse root $v = 1 / 2$ on the selected branch.

Verification

1.1givenalgebra

Direct multiplication gives $A u_{*} = (2, - 1)$ and $(u_{*, 1}^{3}, u_{*, 2}^{3}) = (1, 0)$ , so $f_{h} = F_{h} (u_{*}) = (3, - 1)$ . The restricted iterate is $I u_{*} = 1 / 2$ , while $R f_{h} = 3 - 1 = 2$ .

2.1F1step 1.1algebra

The Galerkin coarse value at the restricted iterate is $F_{H} (1 / 2) = 1 + 1 / 4 = 5 / 4$ . Thus [F1] gives $τ (u_{*}) = F_{H} (I u_{*}) - R F_{h} (u_{*}) = 5 / 4 - 2 = - 3 / 4$ and the tau-corrected coarse right side is $R f_{h} + τ (u_{*}) = 2 - 3 / 4 = 5 / 4$ .

3.1givenF2step 1.1step 2.1algebra∎

Since $F_{H} (1 / 2) = 5 / 4$ , the exact selected coarse solution is $v = I u_{*} = 1 / 2$ . Therefore $P (v - I u_{*}) = 0$ and the fine correction leaves $u_{*}$ unchanged; the pre/post residual smoothers also leave it fixed because $F_{h} (u_{*}) = f_{h}$ . This is the instance of [F2] with the actual tau value verified above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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.