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.

✓ 4 results · all verified · 4 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; all 4 also cleared it.

Adaptive finite-element methods — Examples

1 · Prerequisites

2 · Summary

These finite checks demonstrate the exact descending-prefix bulk rule, P0 data-oscillation projection on a reference triangle, nonconstant conormal-flux oscillation across a coefficient interface, and failure of the stated sufficient small-mesh inequality for a prescribed convection constant. Each verification uses the definitions and hypotheses on adaptive-finite-element-methods. The coefficient and convection examples do not assert general convergence or failure of convergence.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

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

A coefficient jump creates nonzero edge-flux oscillation

Example

Assume Countable Choice for the cited Sobolev/L2 interface.

Let $E = {(0, y) : 0 \leq y \leq 1}$ be shared by $K^{-} = conv {(- 1, 0), (0, 0), (0, 1)}$ and $K^{+} = conv {(1, 0), (0, 0), (0, 1)}$ . Set $A^{-} = 1$ , $A^{+} = 1 + y$ , and $U (x, y) = x$ . On each triangle $A$ is positive and Lipschitz; its traces differ on $E$ .

Facts & Assumptions

[A1]

Countable Choice is the background assumption in the cited Sobolev and $L^{2}$ suppliers (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Given: Countable Choice, The piecewise-Lipschitz coefficient interface and projected edge flux oscillation of Residual indicators and data oscillation for P1 AFEM.

[F1]

For a scalar diffusion coefficient, the outward conormal flux on a side is $A \nabla U \cdot n$ ; edge oscillation is the squared $L^{2}$ distance of the outward flux sum from its edge mean (Residual indicators and data oscillation for P1 AFEM).

Verification

1.1A1F1givenalgebra

The gradient is $\nabla U = (1, 0)$ . The outward normals on $E$ are $n^{-} = (1, 0)$ and $n^{+} = (- 1, 0)$ , so the sum of outward conormal fluxes is $J_{E} (y) = 1 - (1 + y) = - y$ . Its edge mean on $[0, 1]$ is $- 1 / 2$ .

2.1step 1.1algebra∎

Since $h_{E} = 1$ , $h_{E} ∥ J_{E} - Π_{E}^{0} J_{E} ∥_{L^{2} (E)}^{2} = \int_{0}^{1} (y - \frac{1}{2})^{2} d y = \frac{1}{12} > 0.$ Thus the coefficient interface creates a nonzero projected edge contribution. No general reliability or complexity assertion for this coefficient model follows from the example.

Finite check

The edge integral is the elementary variance of $y$ on $[0, 1]$ , equal to $1 / 12$ .

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

A coarse mesh can miss the convection smallness condition

Example

Assume Countable Choice for the cited Sobolev/L2 interface.

Fix a positive mesh diameter $h_{0}$ , exponent $s > 0$ , and a stipulated positive dual-pickup constant $C_{D}$ . The sufficient small-mesh parameter in Quasi-orthogonality for constant convection on a fine initial mesh is $μ = C_{D} h_{0}^{s} ∣ b ∣$ .

Facts & Assumptions

[A1]

Countable Choice is the background assumption in the cited Sobolev and $L^{2}$ suppliers (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Given: Countable Choice, A prescribed mesh scale $h_{0} > 0$ , $s > 0$ , $C_{D} > 0$ , and a constant divergence-free vector $b \in R^{2}$ .

[F1]

The nonsymmetric quasi-orthogonality estimate assumes $μ = C_{D} h_{0}^{s} ∣ b ∣ < 1$ (Quasi-orthogonality for constant convection on a fine initial mesh).

Verification

1.1A1F1givenconstructalgebra

Choose any unit vector $e$ and set $b = 2 (C_{D} h_{0}^{s})^{- 1} e$ . This is constant and divergence-free, and direct substitution gives $μ = 2$ .

2.1step 1.1algebra∎

The strict sufficient condition $μ < 1$ therefore fails on this prescribed mesh. This only shows that the stated sufficient estimate cannot be invoked from its hypotheses; it does not imply failure of convergence or of the PDE solution.

Finite check

The substitution is exact: $C_{D} h_{0}^{s} \cdot 2 (C_{D} h_{0}^{s})^{- 1} = 2$ .

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

A deterministic Dörfler mark on three cells

Example

Take squared cell indicators $(9, 4, 1)$ in the stated identifier order and $θ_{E} = 3 / 5$ .

Facts & Assumptions

Given: Three nonnegative squared indicators and the deterministic prefix rule of Dorfler marking and conforming newest-vertex refinement.

[F1]

Dörfler marking selects the shortest descending-value prefix whose sum reaches the declared fraction of the total (Dorfler marking and conforming newest-vertex refinement).

Verification

1.1F1givenalgebra

The total is $9 + 4 + 1 = 14$ , so the threshold is $(3 / 5) 14 = 42 / 5 = 8.4$ . The sorted descending prefix sums are $9, 13, 14$ .

2.1step 1.1algebra∎

The first prefix already has sum $9 \geq 8.4$ , while the empty prefix has sum $0 < 8.4$ . Thus the unique minimal mark is the first cell, regardless of the later tie rule.

Finite check

The three prefixes are exactly $\emptyset$ , ${1}$ , ${1, 2}$ and ${1, 2, 3}$ with sums $0, 9, 13, 14$ ; the first threshold-crossing prefix has cardinality one.

Adaptive finite-element methods — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A coefficient jump creates nonzero edge-flux oscillation

Example

Facts & Assumptions

Verification

Finite check

A coarse mesh can miss the convection smallness condition

Example

Facts & Assumptions

Verification

Finite check

A deterministic Dörfler mark on three cells

Example

Facts & Assumptions

Verification

Finite check

Projected data oscillation on a reference triangle

Example

Facts & Assumptions

Verification

Finite check

Sources