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

✓ 3 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Multigrid methods and complexity — Examples

1 · Prerequisites

2 · Summary

The examples calculate a coarse correction that removes a piecewise-linear error exactly, expand the V- and W-cycle work recurrences for four-to-one coarsening, and check a finite Poisson mode against the uniform two-grid estimate. Every convergence claim uses the A-page hypotheses; arithmetic work and convergence remain separate.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A linear error on the one-dimensional Poisson coarse space is removed exactly

Example

Consider the homogeneous weak Dirichlet form for $- u^{''}$ on $(0, 1)$ , in the sense of Weak Dirichlet solutions for a divergence-form operator and Uniformly elliptic divergence-form operators and their sesquilinear forms, and the uniform mesh with four fine intervals. The continuous piecewise-linear nodal basis has interior hat functions $ϕ_{1}, ϕ_{2}, ϕ_{3}$ . Its stiffness matrix is

$A_{h} = 4 (\begin{array}{ccc} 2 & - 1 & 0 \\ - 1 & 2 & - 1 \\ 0 & - 1 & 2 \end{array}) .$

The coarser mesh has one interior node. Its piecewise-linear prolongation is $P = (1 / 2, 1, 1 / 2)^{T}$ . The vector $e = (1, 2, 1)^{T} = 2 P$ is represented exactly on the coarse space, so one exact Galerkin correction removes it.

This calculation uses the homogeneous weak-form branch, whose functional-space interface assumes Countable Choice. It establishes the finite matrix identity without asserting solution existence for a forcing or a finite-element error estimate, and it makes no claim about inhomogeneous trace data.

Facts & Assumptions

Given: The interval $(0, 1)$ , its zero-boundary weak Poisson form, the four-interval uniform mesh, and its continuous piecewise-linear nodal basis.

[F1]

Weak Dirichlet solutions for a divergence-form operator: in the homogeneous branch, a weak solution is an $H_{0}^{1}$ class satisfying $a (u, v) = F (v)$ for every test function; that branch assumes Countable Choice. Only the definition of the weak form is used here, not an existence theorem.

[F2]

Uniformly elliptic divergence-form operators and their sesquilinear forms: with coefficient $a^{11} = 1$ and $b = c = 0$ , the form is $a (u, v) = \int_{0}^{1} u^{'} (x) v^{'} (x) d x$ in the real case.

[F3]

Galerkin coarse matrices and the exact coarse-correction error map: $A_{H} = P^{T} A_{h} P$ and $C = I - P A_{H}^{- 1} P^{T} A_{h}$ when $A_{H}$ is invertible.

[F4]

Continuous piecewise-affine functions with zero endpoints lie in H1-zero: each continuous piecewise-affine function on $[0, 1]$ vanishing at $0$ and $1$ belongs to $H_{0}^{1} (0, 1)$ .

[A1]

Assume The Axiom of Countable Choice ( ${A C}_{ω}$ ) for the homogeneous Sobolev interface in [F1]. The finite matrix calculation uses this homogeneous branch.

Verification

1.1givenA1F1F2F4algebra

Each fine nodal hat is continuous piecewise affine and zero at both endpoints, so [F4] places it in $H_{0}^{1} (0, 1)$ , the test space in [F1] under [A1]. On each interval its derivative is constant. For $i = j$ , the integral $\int ϕ_{i}^{'} ϕ_{i}^{'}$ receives $1 / h$ from each of its two adjacent intervals, giving $2 / h = 8$ ; for adjacent indices, the shared interval contributes $- 1 / h = - 4$ ; nonadjacent supports have zero derivative-product integral. Thus the matrix of $a (\cdot, \cdot)$ is the displayed $A_{h}$ .

2.1F3step 1.1algebra

With $h = 1 / 4$ , direct multiplication gives $A_{h} P = (0, 4, 0)^{T}$ and $A_{H} = P^{T} A_{h} P = 4$ . Therefore [F3] gives $C = I - P (0, 1, 0)$ , which maps $(x_{1}, x_{2}, x_{3})^{T}$ to $(x_{1} - x_{2} / 2, 0, x_{3} - x_{2} / 2)^{T}$ .

3.1step 2.1algebra∎

For $e = (1, 2, 1)^{T}$ , step 2.1 yields $C e = (1 - 1, 0, 1 - 1)^{T} = 0$ . The error is exactly the prolongation of its single coarse value $2$ , so the exact coarse correction removes it.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

V- and W-cycle work under two-dimensional four-to-one coarsening

Example

Assume a two-dimensional hierarchy with levels $j = 0, \dots, L$ of sizes $N_{j} = 4^{j}$ , so the finest level has $N = N_{L} = 4^{L}$ unknowns and each coarsening step reduces the size by four. Suppose each level has constant $c > 0$ work per unknown, the base solve has bounded positive cost, and the cycle is as in Finite recursive Galerkin V- and W-cycle for an SPD hierarchy. The V-cycle has one coarse call; the W-cycle has two. Both have $Θ (N)$ arithmetic work under these hypotheses, with different geometric sums.

Facts & Assumptions

Given: Integer $L \geq 1$ , level sizes $N_{j} = 4^{j}$ for $0 \leq j \leq L$ , $N = N_{L} = 4^{L}$ , per-level work $c N_{j}$ with $c > 0$ , a bounded positive coarsest solve, and the V/W call counts $γ = 1, 2$ .

[F1]

Work recurrence for fixed-coarsening multigrid cycles in all three regimes: for $q = 2^{d} = 4$ , work is $Θ (N)$ when $γ < 4$ .

Verification

1.1givenF1algebra

For the V-cycle, $T_{V} (N) = c N + T_{V} (N / 4)$ . Repeated substitution gives $T_{V} (N) = c N \sum_{r = 0}^{L - 1} 4^{- r} + T_{V} (1) .$ The sum lies between $1$ and $4 / 3$ , and $T_{V} (1) = Θ (1)$ , so $T_{V} (N) = Θ (N)$ . This is also the $γ = 1 < 4$ case of [F1].

2.1givenF1algebra∎

For the W-cycle, $T_{W} (N) = c N + 2 T_{W} (N / 4)$ , so $T_{W} (N) = c N \sum_{r = 0}^{L - 1} 2^{- r} + 2^{L} T_{W} (1) .$ The sum lies between $1$ and $2$ , while $2^{L} = \sqrt{N}$ ; consequently both terms are $O (N)$ and the first is a positive $c N$ lower bound. Hence $T_{W} (N) = Θ (N)$ , agreeing with [F1] because $γ = 2 < 4$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

One high-frequency mode in the finite one-dimensional Poisson two-grid cycle

Example

Use the four-interval mesh from the homogeneous weak Dirichlet Poisson form on $(0, 1)$ and the exact piecewise-linear coarse correction. Here $A_{h} = 4 T_{3}$ , where $T_{3} = (\begin{array}{ccc} 2 & - 1 & 0 \\ - 1 & 2 & - 1 \\ 0 & - 1 & 2 \end{array})$ , and $P = (1 / 2, 1, 1 / 2)^{T}$ . For the error $e = (1, 0, - 1)^{T}$ , the coarse correction leaves the vector unchanged, while one Richardson sweep with step $1 / λ_{\max} (A_{h})$ damps it by $\sqrt{2} - 1$ . The symmetric two-grid error map therefore sends this particular mode to $(3 - 2 \sqrt{2}) e$ . The level-uniform theorem bounds the full operator norm by $2 / 3$ for one sweep, not merely this single mode.

The calculation uses the homogeneous weak-form convention and makes no claim about solution existence or finite-element discretization error.

Facts & Assumptions

Given: The homogeneous weak Dirichlet Poisson form on $(0, 1)$ , the four-interval fine mesh with $A_{h} = 4 T_{3}$ , $T_{3} = (\begin{array}{ccc} 2 & - 1 & 0 \\ - 1 & 2 & - 1 \\ 0 & - 1 & 2 \end{array})$ , coarse prolongation $P = (1 / 2, 1, 1 / 2)^{T}$ , the error $e = (1, 0, - 1)^{T}$ , and one Richardson sweep.

[F1]

Weak Dirichlet solutions for a divergence-form operator: the homogeneous weak Dirichlet problem uses $u \in H_{0}^{1} (0, 1)$ and the form identity against every $H_{0}^{1}$ test function; this branch assumes Countable Choice.

[F2]

Uniformly elliptic divergence-form operators and their sesquilinear forms: for the real Poisson coefficients $a^{11} = 1$ , $b = c = 0$ , the form is $a (u, v) = \int_{0}^{1} u^{'} v^{'} d x$ .

[F3]

Galerkin coarse matrices and the exact coarse-correction error map: $A_{H} = P^{T} A_{h} P$ and $C = I - P A_{H}^{- 1} P^{T} A_{h}$ when $A_{H}$ is invertible.

[F4]

The symmetric two-grid error map from a pre-smoother and Galerkin correction: the symmetric cycle map is $E = S^{*_{A_{h}}} C S$ .

[F5]

The symmetric 1D Poisson two-grid cycle is uniformly contractive: the symmetric 1D Poisson map has $∥ E ∥_{A_{h}} \leq 2 / (2 ν + 1)$ for every $ν \geq 1$ and every even $N \geq 4$ .

[F6]

Continuous piecewise-affine functions with zero endpoints lie in H1-zero: each continuous piecewise-affine function on $[0, 1]$ vanishing at $0$ and $1$ belongs to $H_{0}^{1} (0, 1)$ .

[A1]

Assume The Axiom of Countable Choice ( ${A C}_{ω}$ ) for the homogeneous Sobolev interface in [F1]. This example uses the homogeneous branch and makes no inhomogeneous trace claim.

Verification

1.1givenA1F1F2F6algebra

The fine nodal hats are continuous piecewise affine and vanish at both endpoints, so [F6] puts them in the homogeneous test space of [F1] under [A1]; [F2] then gives their form as $\int_{0}^{1} u^{'} v^{'}$ . Direct determinant expansion gives $\det (t I - T_{3}) = t^{3} - 6 t^{2} + 10 t - 4 = (t - 2) (t^{2} - 4 t + 2),$ so $λ_{\max} (A_{h}) = 4 (2 + \sqrt{2})$ , while direct multiplication gives $A_{h} e = 8 e$ . Thus one pre-sweep $S = I - A_{h} / λ_{\max} (A_{h})$ sends $e$ to $(1 - 8 / [4 (2 + \sqrt{2})]) e = (\sqrt{2} - 1) e$ .

2.1F3F4step 1.1algebra

Direct multiplication gives $A_{h} P = (0, 4, 0)^{T}$ and $A_{H} = P^{T} A_{h} P = 4$ . Hence $C = I - P (0, 1, 0)$ and $C e = e$ , since the middle component of $e$ is zero. Since $S = I - A_{h} / λ_{\max}$ is symmetric and commutes with $A_{h}$ , its $A_{h}$ -adjoint $A_{h}^{- 1} S^{T} A_{h}$ equals $S$ . Thus [F4] gives $E e = (\sqrt{2} - 1)^{2} e = (3 - 2 \sqrt{2}) e$ .

3.1F4F5step 2.1algebra∎

Since $3 - 2 \sqrt{2} < 2 / 3$ (equivalently $49 < 72$ after multiplying by positive quantities and squaring), this mode is damped by less than $2 / 3$ . [F5] with $ν = 1$ bounds the full energy operator norm by $2 / 3$ , including every fine-grid mode.

Multigrid methods and complexity — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A linear error on the one-dimensional Poisson coarse space is removed exactly

Example

Facts & Assumptions

Verification

V- and W-cycle work under two-dimensional four-to-one coarsening

Example

Facts & Assumptions

Verification

One high-frequency mode in the finite one-dimensional Poisson two-grid cycle

Example

Facts & Assumptions

Verification

Sources