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.
Linear elasticity, nearly incompressible limits and locking — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Absolute Values Completions and P Adic Numbers
- Areas of Elementary Plane Figures
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Céa and Aubin–Nitsche error estimates
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Lp Spaces and Test-Function Conventions
- 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
- Continuity, IVT, EVT, and Uniform Continuity
- Convexity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Darboux, L'Hôpital, and Taylor's Theorem
- Decomposition Inertia and Frobenius
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Distributions Test Functions and Differentiation
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces Adjoint Operators and Annihilators
- 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
- Finite Probability and the Probabilistic Method
- Finite-element meshes and interpolation
- Foundations of the Real Numbers for Analysis
- Fourier Multipliers and Sobolev Characterisations
- Fourier Transform Convolution and Approximate Identities
- Fredholm Elliptic Problems and the Elliptic Spectrum
- Fubini and Change of Variables
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Harmonic Functions and Mean Values in Rn
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper and Parameter-Dependent Multiple Integrals
- Improper Integrals
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lax--Milgram and Weak Elliptic Solutions
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear elasticity, nearly incompressible limits and locking
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed finite elements and Stokes stability
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Orthonormal Bases, Parseval and Fourier Series
- Outer Measure and the Caratheodory Extension Theorem
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Schwartz Space and the Plancherel Theorem
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Smooth Approximation and Sobolev Extension
- Smooth Manifolds and Smooth Maps
- Smooth Partitions of Unity and Exhaustions
- Sobolev Poincare and Morrey Inequalities
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tangent Cotangent and the Differential
- Tempered Distributions and the Fourier Transform
- The Analytic Hahn Banach Theorem
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Inverse and Implicit Function Theorems
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Derivatives and Sobolev Spaces
2 · Summary
The examples compute a manufactured shear state on a clamped rectangle, identify the rigid translations and rotations in a free-body stiffness kernel, and exhibit a fixed four-triangle P1 displacement space whose only pointwise divergence-free field is zero. A smooth solenoidal load then forces the P1 solution to vanish as on that fixed mesh. The mini-element comparison uses the parameter-uniform best-approximation theorem; no mesh-uniform P1 rate is claimed.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Rigid motions in a free-body stiffness nullspace
Statement
Let , , be a connected polygonal or polyhedral domain with a finite conforming affine simplicial mesh and no essential boundary constraints. Define the continuous P1 vector space and its global nodal basis . For constants and , set , , and . For every infinitesimal rigid motion , with and , its nodal coefficient vector lies in . Thus the range of any complete nullspace basis supplied to Algebraic gauge for a rigid-body stiffness nullspace must contain these translation and rotation vectors. This example does not claim they exhaust the nullspace on every mesh.
Facts & Assumptions
Given: A conforming affine simplicial mesh, its global continuous P1 vector space without essential boundary constraints, and the displayed isotropic stiffness bilinear form.
The algebraic gauge procedure requires a complete basis of the stiffness kernel and a compatible load before it is applied. (Algebraic gauge for a rigid-body stiffness nullspace)
Verification
On each nondegenerate simplex, an affine map is uniquely determined by its values at the affinely independent vertices, so its nodal P1 interpolant equals it. On each shared face the affine traces are determined by the same face-vertex values, so they agree and define a global continuous member of .
Since is skew-symmetric, and . Thus the stiffness bilinear form pairs to zero with every test basis function, which is exactly in coefficient coordinates. By [F1], every complete gauge basis must span these null vectors, although other null modes are not excluded here.
A manufactured shear field on a clamped rectangle
Statement
Assume Countable Choice. On , clamp the left edge and prescribe traction on the other three open edges . Let and be constants and set . The stress is constant and satisfies , , and on the right edge, on the top edge, and on the bottom edge. This is a manufactured linear-elasticity solution; no uniqueness result for partial Dirichlet data is asserted.
Facts & Assumptions
Given: Countable Choice; the linear-elasticity strain and stress conventions of Linear isotropic elasticity: displacement form and data; the square ; constant ; and .
Countable Choice is inherited through the imported model definition; the direct matrix and traction computations use no choice. (The Axiom of Countable Choice ())
The symmetric gradient is and . (Linear isotropic elasticity: displacement form and data)
Verification
The gradient of is , so and . Hence [F1] gives , independent of .
The stress is constant, so its row-wise divergence is zero. The displacement vanishes at . Multiplication by the outward unit normals , , and on the right, top, and bottom edges gives the three displayed tractions.
A fixed-mesh P1 volumetric-locking obstruction
Statement
Assume Countable Choice. On , let and split the square into the four triangles joining to consecutive corners. The continuous P1 vector space with zero boundary values has no nonzero elementwise divergence-free field. Choose a nonzero smooth compactly supported divergence-free displacement and set . Then solves the continuous model with for every finite , but the P1 displacement Galerkin solutions on this fixed mesh tend to zero as , so their -norm error tends to . The mini mixed pair on the same mesh retains the -uniform best-approximation estimate of Uniform mini-element stability through the incompressible limit. This is a fixed-mesh obstruction, not a mesh-uniform P1 rate.
Facts & Assumptions
Given: Countable Choice; the displacement model, its energy theorem, the mini mixed formulation and stability theorem; and the four-triangle fan mesh specified in the statement.
Countable Choice is inherited through the continuous Hilbert-space solution theorem; the finite-mesh calculation and compactness argument use finite-dimensional subsequence extraction. (The Axiom of Countable Choice ())
For and finite , the displacement solution is unique, has the stated energy identity, and satisfies a uniform bound. (Dirichlet elasticity energy bound and Galerkin estimate)
The mixed mini-element problem has a -uniform solution and best-approximation bound on a common shape-regular mesh family. (Uniform mini-element stability through the incompressible limit)
The P1-bubble/P1 mini-element uses continuous P1 vector functions with zero trace plus cell bubbles, and mean-zero continuous P1 pressures. (The conforming P1-bubble/P1 mini element)
The integral pairing obeys . (Cauchy-Schwarz inequality for )
is the -closure of . (Zero-boundary Sobolev space as a norm closure)
For zero-boundary fields, . (The homogeneous Dirichlet strain identity)
Verification
Set for and otherwise. At each endpoint every derivative from the interior is a finite sum of reciprocal-distance powers multiplied by for some , hence tends to zero; so . Put and . Equality of mixed derivatives gives . Since and , the mean value theorem gives with ; hence . Thus and is compactly supported in .
Let . For , integration by parts and symmetry of give . By [A1, F5], choose such tests converging to any given in ; [F4] makes both pairings continuous under this convergence, so the identity holds for every .
A P1 vector field in this mesh vanishes at every boundary vertex and is determined by its center value . On the bottom triangle the edge vectors from the center to its corners are and ; its affine gradient maps both to . Subtracting gives the first column of zero, and adding gives the second column , so divergence is . On the right triangle the edge vectors are and ; subtraction gives the second column zero and addition the first column , hence divergence is . On the top triangle the edge vectors are and ; subtraction gives the first column zero and addition the second column , hence divergence is . On the left triangle the edge vectors are and ; subtraction gives the second column zero and addition the first column , hence divergence is . If all four divergences vanish, then , so the elementwise divergence-free subspace is exactly .
Since , the volumetric term vanishes and step 1.2 gives for every and every finite . By [F1], this identifies the same nonzero as the unique continuous solution for each such .
Let be the P1 Galerkin solution, which exists uniquely by [F1]. Testing with , using [F6] with , and applying [F4] gives and . Thus along every sequence the discrete solutions are bounded in the finite-dimensional P1 space and have a convergent subsequence; the divergence of its limit is zero because the divergence norms tend to zero and convergence in implies convergence of divergence in . The limit is zero by step 1.3. If the full family did not converge to zero, a sequence bounded away from zero would have such a zero-convergent subsequence, a contradiction. Hence and the reverse triangle inequality gives .
The mini mixed comparison is exactly the scoped result [F2] under the spaces [F3]; its estimate keeps the best-approximation term and its constant is independent of on this mesh family. No conclusion about a P1 rate as is used.