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.
Data, operator, discretization, and solve errors — Examples and Counterexamples
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compact linear inverse maps and the Picard criterion
- Compact Operators and Riesz Schauder Theory
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Norms and Realification
- Complex Subspace Realification
- Complexification, Realification and Real Structures
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Data, operator, discretization, and solve errors
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Foundations of the Real Numbers for Analysis
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Inverse maps, identifiability, and stability
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Simple Field Extensions and the Construction of the Complex Numbers
- Subspaces, Products, and Quotients
- Suprema and Infima
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Logical flowchart
3 · Definitions, theorems and proofs
None yet.
4 · Examples, counterexamples and false statements
Vanishing data errors with persistent small-singular-value reconstruction error
Example
For every integer , let with the Euclidean inner product and let Set , exact data , noise , noise bound , and regularization coefficient . The observed data are , and the returned output is the exact Tikhonov output The smallest singular value of is , while . Nevertheless At each resolution the discrete operator equals the forward operator and the discretized datum is formed exactly before adding noise, so the operator, pre-inversion, and algebraic-solve channels vanish; only data perturbation remains. Thus vanishing noise alone does not force vanishing reconstruction error when the retained singular values shrink and is chosen as above.
Example references
Facts & Assumptions
Given: For each , the real finite-dimensional spaces , the diagonal map , , , , , and .
Error budget for computed Tikhonov inversion: The budget uses , , , , and the five bias, data, operator, pre-inversion, and solve vectors; its shifted normal operators are assumed bijective.
Bounded finite rank operators are compact: Every bounded linear operator whose range has a finite ordered basis is compact.
Verification
Given: The finite matrices and data in the Example, with the standard coordinate vectors in .
The map is bounded and has range , which has the finite ordered basis . Hence is compact by [F2]. Its adjoint is , and is diagonal with positive entries for ; therefore the adjoints and bijective shifted normal operator required by [F1] are supplied in this finite model.
Let be the last coordinate vector. Then , , and . Solving this one diagonal coordinate gives .
Since and , the bias, pre-inversion, and operator channels are zero. Since is the exact discrete Tikhonov output, the solve channel is zero. The only nonzero channel is the data vector . Therefore , while and the smallest singular value is .
The scalar data-noise allowance in the general budget is , so it does not force the exact errors in step 3.1 to tend to zero. The sequence has resolved forward data at every level and asserts no convergence theorem for a fixed infinite-dimensional discretization.
Early stopping leaves a nonzero Tikhonov normal residual
Example
Let with the usual inner product, let , let , , , and set . The exact Tikhonov output is , and its normal equation is . Apply one Richardson step with step size from : The returned output has exact normal-equation residual and reconstruction error . The bias, data, operator, and pre-inversion channels are zero; only the algebraic solve channel is nonzero.
Example references
Facts & Assumptions
Given: The one-dimensional real Hilbert spaces , the identity maps , , , , , , initial iterate , and Richardson step size .
Error budget for computed Tikhonov inversion: The solve vector is , and the exact normal residual is .
Bounded finite rank operators are compact: Every bounded linear operator whose range has a finite ordered basis is compact.
Verification
Given: The scalar data and iteration in the Example.
The identity is bounded and has the finite range basis , so it is compact by [F2]. The shifted normal operator is , which is bijective with inverse ; hence the finite scalar instance satisfies [F1].
One Richardson step for from gives . Substitution into the residual definition gives , while the exact regularized output is .
The truth bias and data perturbation vanish because . Since , and the regularized-operator difference vanishes; the pre-inversion channel is therefore also zero. The solve channel is , so its norm equals the reconstruction error and is at most the residual allowance .