Alphabeta Math
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.

✓ 3 results · all verified · 2 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. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Crouzeix–Raviart finite elements — Examples

1 · Prerequisites

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 H1 function whose gradient is not in H1/2. The last example marks the strict trace-regularity boundary and explicitly lies outside the method's L2-load error theorem.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A zero-boundary solution below the CR trace regularity threshold

Statement refuted

Every u∈H01((0,1)2) belongs to H1+r((0,1)2) for some r∈(1/2,1].

Facts & Assumptions

Given: Countable Choice, Ω=(0,1)2, the standard smooth step σ of The standard smooth step function, the fractional Sobolev convention of Fractional Sobolev regularity on a simplex, and H01 as the W1,2 closure of Cc∞(Ω).

[A1]

Countable Choice is an assumption of the fractional Sobolev convention and local simplex trace interface used below. (The Axiom of Countable Choice (ACω), Fractional Sobolev regularity on a simplex, Fractional face traces and cellwise Green identity on a simplex)

[F1]

The standard smooth step σ is smooth, takes values in [0,1], equals zero on (−∞,0], and equals one on [1,∞). (The standard smooth step function)

[F2]

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)

[F3]

The local simplex trace result is stated only for gradient regularity r>1/2. (Fractional face traces and cellwise Green identity on a simplex)

[F4]

Membership in H1+r(Ω) requires every weak first derivative to lie in Hr(Ω) with the stated Gagliardo seminorm. (Fractional Sobolev regularity on a simplex)

[F5]

At r=1, the regularity definition sets H2(Ω)=W2,2(Ω), so membership implies Δu∈L2(Ω); Holder's inequality also bounds the weak Poisson functional by ∥∇u∥2∥∇v∥2. (Fractional Sobolev regularity on a simplex, Holder's inequality for integrals, including the endpoint cases)

Counterexample

Set χ(x):=1−σ(4x−1) for x∈[0,1] and define u(x,y)=χ(x)x3/4y(1−y). By [F1], χ is smooth, equals one on [0,1/4], and equals zero on [1/2,1].

1.1F1givenalgebra

On 0<x<1/4, writing c(y)=y(1−y), one has ∂xu=34c(y)x−1/4,∂yu=(1−2y)x3/4. Everywhere else the cutoff and its derivative are bounded. Since u and ∂yu are square integrable and ∣∂xu∣2≤C(1+x−1/2), the weak first derivatives lie in L2(Ω); the classical interior derivatives give the distributional derivatives because test functions are compactly supported away from the boundary. Thus u∈H1(Ω).

1.2F1givenalgebra

To prove the zero-boundary condition, let θϵ(t):=σ((t−ϵ)/ϵ). By [F1], it is smooth, zero for t≤ϵ, and one for t≥2ϵ. Since σ′ is continuous and vanishes outside [0,1], ∥θϵ′∥∞≤C/ϵ. Set ηϵ(x,y)=θϵ(x)θϵ(y)θϵ(1−y). Each ηϵu is smooth and compactly supported in Ω, since the x cutoff removes the only nonsmooth boundary point and χ vanishes near x=1. Write u−ηϵu=(1−θϵ(x))u+θϵ(x)(1−θϵ(y)θϵ(1−y))u. In the first term, all support lies in x<2ϵ; the squared L2 and derivative errors are bounded by Cϵ2(3/4)−1=Cϵ1/2, including the ϵ−1u cutoff derivative. In the second term, support lies in the two strips of width 2ϵ near y=0,1. There ∣u∣≤Cx3/4dist⁡(y,{0,1}) and its first derivatives are bounded by Cx3/4+Cx−1/4dist⁡(y,{0,1}); integrating the strips shows the squared errors and cutoff-derivative terms are O(ϵ). Thus ηϵu→u in H1(Ω), so the closure definition gives u∈H01(Ω).

2.1A1F2step 1.1givenalgebra

Choose 0<δ<1/12 so small that c(y′)/c(y)≤1.05 whenever 0<x<δ, 1/3≤y≤2/5, and y≤y′≤y+x. For the pairs below, x′≤3x<1/4, so both points lie where χ=1; also c(y) is bounded below by a positive constant on this y interval. For 2x≤x′≤3x and y≤y′≤y+x, the values of ∂xu(x,y) and ∂xu(x′,y′) then differ by at least 34c(y)x−1/4(1−1.05 2−1/4). Thus ∣∂xu(x,y)−∂xu(x′,y′)∣≥Cx−1/4. Also ∣(x,y)−(x′,y′)∣≤5x. By [F2], restricting the H1/2 Gagliardo integral to these pairs gives a lower bound C∫0δx−1/2x−3 x2 dx=C∫0δx−3/2 dx=∞, where the two factors of x are the lengths of the x′ and y′ intervals. Thus ∂xu∉H1/2(Ω).

3.1A1F4step 2.1givenalgebra

Let D=diam⁡(Ω)=2. For 1/2<r<1 and x≠y, ∣x−y∣−3=∣x−y∣2r−1∣x−y∣−2−2r≤D2r−1∣x−y∣−2−2r. Integrating gives [q]H1/2(Ω)2≤D2r−1[q]Hr(Ω)2 for every q∈Hr(Ω), so Hr(Ω)⊂H1/2(Ω). If u∈H1+r(Ω) for such an r, [F4] would imply ∂xu∈Hr(Ω) and hence H1/2(Ω), contradicting step 2.1. Thus no exponent r∈(1/2,1) satisfies the refuted claim.

3.2A1F3F5step 1.1step 1.2step 2.1algebra

It remains to exclude r=1. For 0<x<1/4, the cutoff is one and −Δu=316c(y)x−5/4+2x3/4. On 1/3≤y≤2/5, c(y) is bounded below by a positive number, so this classical Laplacian is bounded below by c0x−5/4 for some c0>0; its square has divergent integral at x=0. Since the distributional Laplacian agrees with this classical function in the open square, it has no L2 representative. By [F5], u∉H2(Ω)=W2,2(Ω). The example still defines a bounded weak functional on H01(Ω) by v↦∫Ω∇u⋅∇v, using Holder [F5]; it does not supply the L2 source assumed by the method. Since the example has no H1+r regularity with r>1/2, it does not satisfy the trace hypothesis in [F3], and no normal-gradient trace conclusion is claimed.

4.1step 3.1step 3.2∎

Step 3.1 excludes every r∈(1/2,1), and step 3.2 excludes r=1. These are all exponents in the asserted range, so the counterexample refutes the Statement.

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

One shared face-average degree of freedom

Example

Let F be an interior facet of a finite matching mesh and let ϕF be the global CR basis function indexed by F. It has face mean one on F and zero on every other facet. It is supported only on the two cells incident to F.

Facts & Assumptions

Given: A finite matching mesh, an interior facet F, 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.

[F1]

On a cell K, the face dual polynomial is ϕK,F=1−dλF and its mean is one on F and zero on all other cell facets. (Face averages are unisolvent for the local Crouzeix–Raviart element)

[F2]

The global face basis function is this polynomial on cells incident to F and zero elsewhere. (Interior face means form the global Crouzeix–Raviart degrees of freedom)

Verification

1.1F1given

On either cell incident to F, [F1] gives face mean one on F and zero on that cell's other facets.

2.1F1F2step 1.1givenalgebra∎

On every other cell the function is zero by [F2]. Thus the two traces have matching mean on F, 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 F.

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

A nonzero CR function on a two-triangle square

Example

Split the unit square along the diagonal from (0,0) to (1,1) into K1=conv⁡{(0,0),(1,0),(1,1)} and K2=conv⁡{(0,0),(0,1),(1,1)}. The CR basis function for the diagonal is nonzero and has broken-gradient norm 22. Its boundary edge means vanish, although its boundary traces are not pointwise zero.

The figure uses Cartesian coordinates with x increasing rightward and y upward. The red diagonal is the one interior facet; K1 is below and to its right, and K2 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) {(0,0)}; \node[below right] at (1,0) {(1,0)}; \node[above right] at (1,1) {(1,1)}; \node[above left] at (0,1) {(0,1)}; \node at (0.72,0.35) {K1}; \node at (0.28,0.65) {K2}; \node[red!75!black,above left] at (0.5,0.5) {F}; \end{tikzpicture}

Facts & Assumptions

Given: The two-triangle matching mesh of Ω=(0,1)2 and the homogeneous CR face basis of Interior face means form the global Crouzeix–Raviart degrees of freedom.

[F1]

The local basis polynomial opposite a facet is 1−2λF, and its mean is one on that facet and zero on the other edges. (Face averages are unisolvent for the local Crouzeix–Raviart element)

[F2]

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

1.1F1givenalgebra

On K1, the barycentric coordinate of the vertex (1,0) opposite the diagonal is λ1(x,y)=x−y, so the local polynomial is v1(x,y)=1−2x+2y and ∇v1=(−2,2). On K2, the opposite vertex is (0,1) and λ2(x,y)=y−x, giving v2(x,y)=1+2x−2y and ∇v2=(2,−2).

2.1F1F2step 1.1algebra∎

Each triangle has area 1/2, and both gradient squares have magnitude 8. Thus ∥∇hvh∥22=12(8)+12(8)=8,∥∇hvh∥2=22>0. 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 VhCR,0. On the bottom boundary edge of K1, v1(x,0)=1−2x, which is not identically zero although its edge mean is zero. The example therefore distinguishes the CR mean boundary condition from pointwise Dirichlet values.

Sources