ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A two-by-two inexact assembly ledger

Example

Use Euclidean norm on $X = R^{2}$ and exact matrix/load $A = (\begin{array}{cc} 2 & 1 \\ 1 & 2 \end{array}), f = (\binom{1}{0}) .$ Approximate it by $\tilde{A} = A + E, E = (\begin{array}{cc} 1 / 100 & 0 \\ 0 & - 1 / 100 \end{array}), \tilde{f} = f .$ The exact coercivity and continuity constants are $c = 1$ and $C = 3$ . The defect matrix is $E = diag (1 / 100, - 1 / 100)$ , so $∥ E ∥_{2} = 1 / 100 < 1 / 50$ ; take the conservative certified $δ = 1 / 50$ , load defect $η = 0$ , and $∥ F_{h} ∥ = 1$ . The perturbed solve is $\tilde{u} = (\binom{19900 / 29999}{- 10000 / 29999}),$ while $u = (2 / 3, - 1 / 3)$ . The transfer theorem gives the certified error $∥ u - \tilde{u} ∥_{2} \leq 1 / 49$ ; the exact rational difference is also smaller than $1 / 49$ .

This is a finite algebraic error ledger illustrating how a certified assembly defect enters the perturbation theorem; it does not assert that this particular matrix is a panel matrix from a specified mesh.

Facts & Assumptions

Given: The exact two-dimensional bilinear form, its perturbed matrix, the Euclidean norm, and the transfer theorem.

[F1]

If $δ < c$ , a matrix defect and load defect give the stated Galerkin error bound (A certified matrix defect transfers to a Galerkin error bound).

Proof

1.1givenalgebra

The eigenvectors $(1, 1)$ and $(1, - 1)$ of $A$ have eigenvalues $3$ and $1$ , respectively. Hence $x^{T} A x \geq ∥ x ∥_{2}^{2}$ and $∥ A ∥_{2} = 3$ , so $c = 1$ , $C = 3$ . The defect matrix is diagonal with entries $\pm 1 / 100$ , so $∥ E ∥_{2} = 1 / 100 < 1 / 50$ ; alternatively $∥ E ∥_{2} \leq ∥ E ∥_{F} = \sqrt{2} / 100 < 1 / 50$ . Thus $δ = 1 / 50$ is a certified Euclidean operator defect.

1.2givenalgebra

The determinant of $\tilde{A}$ is $(201 \cdot 199) / 10000 - 1 = 29999 / 10000$ , and its inverse applied to $f$ gives $\tilde{u} = (19900 / 29999, - 10000 / 29999)^{T}$ . The exact inverse of $A$ gives $u = (2 / 3, - 1 / 3)^{T}$ . Their difference is $(- 298 / 89997, - 1 / 89997)^{T}$ , whose squared norm is $88805 / 89997^{2} < 1 / 49^{2}$ because $88805 \cdot 2401 = 213220805 < 8099460009 = 89997^{2}$ .

2.1F1step 1.1step 1.2givenalgebra∎

The discrete space here is the whole two-dimensional space, so the exact Galerkin best-approximation term vanishes; $c = 1$ , $δ = 1 / 50$ , $η = 0$ , and $∥ F_{h} ∥ = 1$ . Applying [F1] gives $∥ u - \tilde{u} ∥_{2} \leq \frac{(1 / 50)}{1 - 1 / 50} = \frac{1}{49},$ which agrees with the direct rational check in step 1.2.

Depends on

A certified matrix defect transfers to a Galerkin error bound

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

Francisco-Javier Sayas, First Steps in the Boundary Element Method (2015 lecture notes) (standard reference, not scraped)
Martin Costabel, Boundary Integral Operators on Lipschitz Domains: Elementary Results (1988) (standard reference, not scraped)