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.
Crouzeix–Raviart finite elements — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Areas of Elementary Plane Figures
- Binary Operations, Monoids, Groups and Subgroups
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Lp Spaces and Test-Function Conventions
- Complex Norms and 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
- Crouzeix–Raviart finite elements
- 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, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite-element meshes and interpolation
- Foundations of the Real Numbers for Analysis
- Fredholm Elliptic Problems and the Elliptic Spectrum
- Fubini and Change of Variables
- 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
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- 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 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
- 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
- Smooth Approximation and Sobolev Extension
- Smooth Manifolds and Smooth Maps
- Smooth Partitions of Unity and Exhaustions
- Sobolev Traces and Zero Boundary Values
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tangent Cotangent and the Differential
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Inverse and Implicit Function Theorems
- 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 isolate one shared face-average degree of freedom, compute the broken-gradient norm of its basis function on a two-triangle square, and exhibit a zero-boundary function whose gradient is not in . The last example marks the strict trace-regularity boundary and explicitly lies outside the method's -load error theorem.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A zero-boundary solution below the CR trace regularity threshold
Statement refuted
Every belongs to for some .
Facts & Assumptions
Given: Countable Choice, , the standard smooth step of The standard smooth step function, the fractional Sobolev convention of Fractional Sobolev regularity on a simplex, and as the closure of .
Countable Choice is an assumption of the fractional Sobolev convention and local simplex trace interface used below. (The Axiom of Countable Choice (), Fractional Sobolev regularity on a simplex, Fractional face traces and cellwise Green identity on a simplex)
The standard smooth step is smooth, takes values in , equals zero on , and equals one on . (The standard smooth step function)
Nonnegative Gagliardo integrals can be restricted to measurable subregions and evaluated by iterated integration. (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability)
The local simplex trace result is stated only for gradient regularity . (Fractional face traces and cellwise Green identity on a simplex)
Membership in requires every weak first derivative to lie in with the stated Gagliardo seminorm. (Fractional Sobolev regularity on a simplex)
At , the regularity definition sets , so membership implies ; Holder's inequality also bounds the weak Poisson functional by . (Fractional Sobolev regularity on a simplex, Holder's inequality for integrals, including the endpoint cases)
Counterexample
Set for and define By [F1], is smooth, equals one on , and equals zero on .
On , writing , one has Everywhere else the cutoff and its derivative are bounded. Since and are square integrable and , the weak first derivatives lie in ; the classical interior derivatives give the distributional derivatives because test functions are compactly supported away from the boundary. Thus .
To prove the zero-boundary condition, let . By [F1], it is smooth, zero for , and one for . Since is continuous and vanishes outside , . Set . Each is smooth and compactly supported in , since the cutoff removes the only nonsmooth boundary point and vanishes near . Write . In the first term, all support lies in ; the squared and derivative errors are bounded by , including the cutoff derivative. In the second term, support lies in the two strips of width near . There and its first derivatives are bounded by ; integrating the strips shows the squared errors and cutoff-derivative terms are . Thus in , so the closure definition gives .
Choose so small that whenever , , and . For the pairs below, , so both points lie where ; also is bounded below by a positive constant on this interval. For and , the values of and then differ by at least Thus . Also . By [F2], restricting the Gagliardo integral to these pairs gives a lower bound where the two factors of are the lengths of the and intervals. Thus .
Let . For and , . Integrating gives for every , so . If for such an , [F4] would imply and hence , contradicting step 2.1. Thus no exponent satisfies the refuted claim.
It remains to exclude . For , the cutoff is one and . On , is bounded below by a positive number, so this classical Laplacian is bounded below by for some ; its square has divergent integral at . Since the distributional Laplacian agrees with this classical function in the open square, it has no representative. By [F5], . The example still defines a bounded weak functional on by , using Holder [F5]; it does not supply the source assumed by the method. Since the example has no regularity with , it does not satisfy the trace hypothesis in [F3], and no normal-gradient trace conclusion is claimed.
Step 3.1 excludes every , and step 3.2 excludes . These are all exponents in the asserted range, so the counterexample refutes the Statement.
One shared face-average degree of freedom
Example
Let be an interior facet of a finite matching mesh and let be the global CR basis function indexed by . It has face mean one on and zero on every other facet. It is supported only on the two cells incident to .
Facts & Assumptions
Given: A finite matching mesh, an interior facet , and the local and global Crouzeix–Raviart bases of Face averages are unisolvent for the local Crouzeix–Raviart element and Interior face means form the global Crouzeix–Raviart degrees of freedom.
On a cell , the face dual polynomial is and its mean is one on and zero on all other cell facets. (Face averages are unisolvent for the local Crouzeix–Raviart element)
The global face basis function is this polynomial on cells incident to and zero elsewhere. (Interior face means form the global Crouzeix–Raviart degrees of freedom)
Verification
On either cell incident to , [F1] gives face mean one on and zero on that cell's other facets.
On every other cell the function is zero by [F2]. Thus the two traces have matching mean on , and all other interior and boundary face means are zero. This is exactly the homogeneous CR condition, and the only nonzero global degree of freedom is the mean on .
A nonzero CR function on a two-triangle square
Example
Split the unit square along the diagonal from to into and . The CR basis function for the diagonal is nonzero and has broken-gradient norm . Its boundary edge means vanish, although its boundary traces are not pointwise zero.
The figure uses Cartesian coordinates with increasing rightward and upward. The red diagonal is the one interior facet; is below and to its right, and is above and to its left.
\begin{tikzpicture}[scale=2,line width=0.7pt,every node/.style={font=\small}] \fill[blue!8] (0,0)--(1,0)--(1,1)--cycle; \fill[green!8] (0,0)--(0,1)--(1,1)--cycle; \draw[gray] (0,0)--(1,0)--(1,1)--(0,1)--cycle; \draw[red!75!black,very thick] (0,0)--(1,1); \fill (0,0) circle (0.025) (1,0) circle (0.025) (1,1) circle (0.025) (0,1) circle (0.025); \node[below left] at (0,0) {}; \node[below right] at (1,0) {}; \node[above right] at (1,1) {}; \node[above left] at (0,1) {}; \node at (0.72,0.35) {}; \node at (0.28,0.65) {}; \node[red!75!black,above left] at (0.5,0.5) {}; \end{tikzpicture}
Facts & Assumptions
Given: The two-triangle matching mesh of and the homogeneous CR face basis of Interior face means form the global Crouzeix–Raviart degrees of freedom.
The local basis polynomial opposite a facet is , and its mean is one on that facet and zero on the other edges. (Face averages are unisolvent for the local Crouzeix–Raviart element)
The global basis function for the only interior facet is supported on its two incident triangles. (Interior face means form the global Crouzeix–Raviart degrees of freedom)
Verification
On , the barycentric coordinate of the vertex opposite the diagonal is , so the local polynomial is and . On , the opposite vertex is and , giving and .
Each triangle has area , and both gradient squares have magnitude . Thus By [F1] its edge means are one on the shared diagonal and zero on the four boundary edges; hence [F2] gives a nonzero element of . On the bottom boundary edge of , , which is not identically zero although its edge mean is zero. The example therefore distinguishes the CR mean boundary condition from pointwise Dirichlet values.